diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 7bbc7598d..f6342951c 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -736,7 +736,35 @@ public:
         return update_app(e, app_fn(e), m);
     }
 
+    bool is_choice_app(expr const & e) {
+        expr const & f = get_app_fn(e);
+        return is_choice(f) || (is_explicit(f) && is_choice(get_explicit_arg(f)));
+    }
+
+    /** \brief Process ((choice f_1 ... f_n) a_1 ... a_k) as
+        (choice (f_1 a_1 ... a_k) ... (f_n a_1 ... a_k))
+    */
+    expr visit_choice_app(expr const & e) {
+        buffer<expr> args;
+        expr f = get_app_rev_args(e, args);
+        bool expl = is_explicit(f);
+        if (expl)
+            f = get_explicit_arg(f);
+        lean_assert(is_choice(f));
+        buffer<expr> new_choices;
+        unsigned num = get_num_choices(f);
+        for (unsigned i = 0; i < num; i++) {
+            expr f_i = get_choice(f, i);
+            if (expl)
+                f_i = mk_explicit(f_i);
+            new_choices.push_back(mk_rev_app(f_i, args));
+        }
+        return visit_choice(mk_choice(new_choices.size(), new_choices.data()), none_expr());
+    }
+
     expr visit_app(expr const & e) {
+        if (is_choice_app(e))
+            return visit_choice_app(e);
         bool expl   = is_explicit(get_app_fn(e));
         expr f      = visit(app_fn(e));
         auto f_t    = ensure_fun(f);
diff --git a/tests/lean/run/nat_bug.lean b/tests/lean/run/nat_bug.lean
new file mode 100644
index 000000000..7d5db5dc5
--- /dev/null
+++ b/tests/lean/run/nat_bug.lean
@@ -0,0 +1,25 @@
+import logic decidable
+using decidable
+
+inductive nat : Type :=
+| zero : nat
+| succ : nat → nat
+
+theorem induction_on {P : nat → Prop} (a : nat) (H1 : P zero) (H2 : ∀ (n : nat) (IH : P n), P (succ n)) : P a
+:= nat_rec H1 H2 a
+
+definition pred (n : nat) := nat_rec zero (fun m x, m) n
+theorem pred_zero : pred zero = zero := refl _
+theorem pred_succ (n : nat) : pred (succ n) = n := refl _
+
+theorem zero_or_succ (n : nat) : n = zero ∨ n = succ (pred n)
+:= induction_on n
+    (or_intro_left _ (refl zero))
+    (take m IH, or_intro_right _
+      (show succ m = succ (pred (succ m)), from congr2 succ (symm (pred_succ m))))
+
+theorem zero_or_succ2 (n : nat) : n = zero ∨ n = succ (pred n)
+:= @induction_on _ n
+    (or_intro_left _ (refl zero))
+    (take m IH, or_intro_right _
+      (show succ m = succ (pred (succ m)), from congr2 succ (symm (pred_succ m))))