diff --git a/src/kernel/metavar.cpp b/src/kernel/metavar.cpp
index 905e2b09c..3f2a6af57 100644
--- a/src/kernel/metavar.cpp
+++ b/src/kernel/metavar.cpp
@@ -317,16 +317,20 @@ bool has_assigned_metavar(expr const & e, metavar_env const & menv) {
 }
 
 local_context add_lift(local_context const & lctx, unsigned s, unsigned n) {
-    if (n == 0) {
+    if (n == 0)
         return lctx;
-    } else if (lctx) {
+#if 0
+    // Remark: I disabled the following simplification.
+    // It impacts negatively the heuristics used in the elaborator.
+    if (lctx) {
         local_entry e = head(lctx);
         // Simplification rule
-        //    lift:(s1+n1):n2 lift:s1:n1 --->  lift:s1:n1+n2
-        if (e.is_lift() && s == e.s() + e.n()) {
+        //    lift:s2:n2 lift:s1:n1 --->  lift:s1:n1+n2   when s1 <= s2 <= s1 + n1
+        if (e.is_lift() && e.s() <= s && s <= e.s() + e.n()) {
             return add_lift(tail(lctx), e.s(), e.n() + n);
         }
     }
+#endif
     return cons(mk_lift(s, n), lctx);
 }
 
diff --git a/src/library/elaborator/elaborator.cpp b/src/library/elaborator/elaborator.cpp
index 4b13a5b7a..b2993c988 100644
--- a/src/library/elaborator/elaborator.cpp
+++ b/src/library/elaborator/elaborator.cpp
@@ -866,13 +866,21 @@ class elaborator::imp {
             local_context  lctx = metavar_lctx(a);
             unsigned i          = head(lctx).s();
             expr t              = head(lctx).v();
+
+            metavar_env & menv  = m_state.m_menv;
+            buffer<unification_constraint> ucs;
+            expr b_type = m_type_inferer(b, ctx, &menv, &ucs);
+            for (auto uc : ucs)
+                m_state.m_queue.push_front(uc);
+            context ctx_with_i = ctx.insert_at(i, g_x_name, b_type); // must add entry for variable #i in the context
+
             std::unique_ptr<generic_case_split> new_cs(new generic_case_split(c, m_state));
             {
                 // Case 1
                 state new_state(m_state);
                 justification new_assumption = mk_assumption();
                 // add ?m[...] == #1
-                push_new_eq_constraint(new_state.m_queue, ctx, pop_meta_context(a), mk_var(i), new_assumption);
+                push_new_eq_constraint(new_state.m_queue, ctx_with_i, pop_meta_context(a), mk_var(i), new_assumption);
                 // add t == b (t << b)
                 expr new_a = t;
                 expr new_b = b;
@@ -923,7 +931,7 @@ class elaborator::imp {
                     imitation = lift_free_vars(b, i, 1);
                 }
                 new_state.m_queue.push_front(c); // keep c
-                push_new_eq_constraint(new_state.m_queue, ctx, mk_metavar(metavar_name(a)), imitation, new_assumption);
+                push_new_eq_constraint(new_state.m_queue, ctx_with_i, mk_metavar(metavar_name(a)), imitation, new_assumption);
                 new_cs->push_back(new_state, new_assumption);
             }
             bool r = new_cs->next(*this);
diff --git a/src/tests/kernel/metavar.cpp b/src/tests/kernel/metavar.cpp
index 11d458735..6ff3bf151 100644
--- a/src/tests/kernel/metavar.cpp
+++ b/src/tests/kernel/metavar.cpp
@@ -439,11 +439,17 @@ static void tst21() {
     expr l  = add_lift(add_lift(m1, 0, 1), 1, 1);
     expr r  = add_lift(m1, 0, 2);
     std::cout << menv.get_type(l) << " " << menv.get_type(r) << "\n";
+#if 0
+    // Leo: I disabled the lift over lift optimization since it was
+    // negatively impacting the heuristics
     lean_assert_eq(l, r);
     lean_assert_eq(add_lift(add_lift(m1, 1, 2), 3, 4),
                    add_lift(m1, 1, 6));
-    lean_assert_ne(add_lift(add_lift(m1, 1, 3), 3, 4),
+    lean_assert_eq(add_lift(add_lift(m1, 1, 3), 3, 4),
                    add_lift(m1, 1, 7));
+    lean_assert_ne(add_lift(add_lift(m1, 0, 3), 3, 4),
+                   add_lift(m1, 1, 7));
+#endif
 }
 
 #define _ mk_placeholder()