diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp
index 6348b99c32..24c1a6ede5 100644
--- a/src/library/type_context.cpp
+++ b/src/library/type_context.cpp
@@ -1699,7 +1699,7 @@ bool type_context::process_assignment(expr const & m, expr const & v) {
                a_{i+k}        =?= b_k
             */
             new_mvar = mk_app(mvar, args.size() - new_v_args.size(), args.data());
-            i        = new_v_args.size();
+            i        = args.size() - new_v_args.size();
         } else if (args.size() < new_v_args.size()) {
             /*
                ?M a_1 ... a_k =?= f b_1 ... b_i b_{i+1} ... b_{i+k}
diff --git a/tests/lean/run/1335.lean b/tests/lean/run/1335.lean
new file mode 100644
index 0000000000..4da99f493e
--- /dev/null
+++ b/tests/lean/run/1335.lean
@@ -0,0 +1,18 @@
+import standard
+namespace int
+
+private lemma sub_nat_nat_elim (m n : ℕ) (P : ℕ → ℕ → ℤ → Prop)
+  (hp : ∀i n, P (n + i) n (of_nat i))
+  (hn : ∀i m, P m (m + i + 1) (-[1+ i])) :
+  P m n (sub_nat_nat m n) :=
+sorry
+
+inductive rel_int_nat_nat : ℤ → ℕ × ℕ → Prop
+| pos : ∀m p, rel_int_nat_nat (of_nat p) (m + p, m)
+| neg : ∀m n, rel_int_nat_nat (neg_succ_of_nat n) (m, m + n)
+
+lemma rel_sub_nat_nat {a b : ℕ} : rel_int_nat_nat (sub_nat_nat a b) (a, b) :=
+/- The next statement kills lean  -/
+sub_nat_nat_elim a b (λ(a b : ℕ) (i : ℤ), rel_int_nat_nat i (a, b)) sorry sorry
+
+end int