diff --git a/src/library/elaborator/elaborator.cpp b/src/library/elaborator/elaborator.cpp
index 7db68e73f..6a00621f7 100644
--- a/src/library/elaborator/elaborator.cpp
+++ b/src/library/elaborator/elaborator.cpp
@@ -908,20 +908,6 @@ class elaborator::imp {
             arg_types.push_back(m_type_inferer(arg(a, i), ctx, menv, ucs));
             push_active(ucs);
         }
-        // Add projections
-        for (unsigned i = 1; i < num_a; i++) {
-            // Assign f_a <- fun (x_1 : T_0) ... (x_{num_a-1} : T_{num_a-1}), x_i
-            state new_state(m_state);
-            justification new_assumption = mk_assumption();
-            expr proj            = mk_lambda(arg_types, mk_var(num_a - i - 1));
-            expr new_a           = arg(a, i);
-            expr new_b           = b;
-            if (!is_lhs)
-                swap(new_a, new_b);
-            push_new_constraint(new_state.m_active_cnstrs, is_eq(c), ctx, new_a, new_b, new_assumption);
-            push_new_eq_constraint(new_state.m_active_cnstrs, ctx, f_a, proj, new_assumption);
-            new_cs->push_back(new_state, new_assumption);
-        }
         // Add imitation
         state new_state(m_state);
         justification new_assumption = mk_assumption();
@@ -987,6 +973,20 @@ class elaborator::imp {
         }
         push_new_eq_constraint(new_state.m_active_cnstrs, ctx, f_a, imitation, new_assumption);
         new_cs->push_back(new_state, new_assumption);
+        // Add projections
+        for (unsigned i = 1; i < num_a; i++) {
+            // Assign f_a <- fun (x_1 : T_0) ... (x_{num_a-1} : T_{num_a-1}), x_i
+            state new_state(m_state);
+            justification new_assumption = mk_assumption();
+            expr proj            = mk_lambda(arg_types, mk_var(num_a - i - 1));
+            expr new_a           = arg(a, i);
+            expr new_b           = b;
+            if (!is_lhs)
+                swap(new_a, new_b);
+            push_new_constraint(new_state.m_active_cnstrs, is_eq(c), ctx, new_a, new_b, new_assumption);
+            push_new_eq_constraint(new_state.m_active_cnstrs, ctx, f_a, proj, new_assumption);
+            new_cs->push_back(new_state, new_assumption);
+        }
     }
 
     /**
diff --git a/tests/lean/induct.lean b/tests/lean/induct.lean
new file mode 100644
index 000000000..240616b30
--- /dev/null
+++ b/tests/lean/induct.lean
@@ -0,0 +1,6 @@
+import macros
+import tactic
+using Nat
+
+theorem add_comm2 (a b : Nat) : a + b = b + a
+:= induction_on b (by skip) _
diff --git a/tests/lean/induct.lean.expected.out b/tests/lean/induct.lean.expected.out
new file mode 100644
index 000000000..6067a56ec
--- /dev/null
+++ b/tests/lean/induct.lean.expected.out
@@ -0,0 +1,8 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Imported 'macros'
+  Imported 'tactic'
+  Using: Nat
+induct.lean:7:0: error: invalid tactic command, unexpected end of file
+Proof state:
+a : ℕ, b : ℕ, n : ℕ, iH : a + n = n + a ⊢ a + (n + 1) = n + 1 + a