diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp
index 3a93d949d5..810e70587a 100644
--- a/src/kernel/type_checker.cpp
+++ b/src/kernel/type_checker.cpp
@@ -42,6 +42,14 @@ class type_checker::imp {
         return ::lean::lift_free_vars(e, d, m_menv.to_some_menv());
     }
 
+    expr instantiate_with_closed(expr const & e, expr const & v) {
+        return ::lean::instantiate_with_closed(e, v, m_menv.to_some_menv());
+    }
+
+    expr instantiate(expr const & e, expr const & v) {
+        return ::lean::instantiate(e, v, m_menv.to_some_menv());
+    }
+
     expr normalize(expr const & e, context const & ctx) {
         return m_normalizer(e, ctx);
     }
@@ -158,9 +166,9 @@ class type_checker::imp {
                 if (closed(abst_body(f_t)))
                     f_t = abst_body(f_t);
                 else if (closed(c))
-                    f_t = instantiate_with_closed(abst_body(f_t), c); // TODO(Leo): m_menv.to_some_menv());
+                    f_t = instantiate_with_closed(abst_body(f_t), c);
                 else
-                    f_t = instantiate(abst_body(f_t), c); // TODO(Leo): m_menv.to_some_menv());
+                    f_t = instantiate(abst_body(f_t), c);
                 i++;
                 if (i == num)
                     return save_result(e, f_t, shared);
@@ -212,9 +220,7 @@ class type_checker::imp {
             {
                 cache::mk_scope sc(m_cache);
                 expr t = infer_type_core(let_body(e), extend(ctx, let_name(e), lt, let_value(e)));
-                return save_result(e,
-                                   instantiate(t, let_value(e)), // TODO(Leo): m_menv.to_some_menv()),
-                                   shared);
+                return save_result(e, instantiate(t, let_value(e)), shared);
             }
         }
         case expr_kind::Value: {
diff --git a/tests/lean/elab1.lean.expected.out b/tests/lean/elab1.lean.expected.out
index 109e6c3361..cbd13c3318 100644
--- a/tests/lean/elab1.lean.expected.out
+++ b/tests/lean/elab1.lean.expected.out
@@ -130,10 +130,47 @@ A : Type, B : Type, a : ?M::0, b : ?M::1, C : Type ⊢ ?M::0[lift:0:3] ≺ C
   Assumed: b
   Assumed: H
 Failed to solve
- ⊢ if ?M::0 ?M::1 ⊤ ≺ b
+ ⊢ if ?M::0 (if (if ?M::3 (if a ⊥ ⊤) ⊤) ⊥ ⊤) ⊤ ≺ b
     Normalize
-     ⊢ ?M::0 ⇒ ?M::1 ≺ b
-        (line: 20: pos: 18) Type of definition 't1' must be convertible to expected type.
+     ⊢ if ?M::0 (?M::3 ∧ a) ⊤ ≺ b
+        Substitution
+         ⊢ if ?M::0 ?M::1 ⊤ ≺ b
+            Normalize
+             ⊢ ?M::0 ⇒ ?M::1 ≺ b
+                (line: 20: pos: 18) Type of definition 't1' must be convertible to expected type.
+            Assignment
+            H1 : ?M::2 ⊢ ?M::3 ∧ a ≺ ?M::1
+                Substitution
+                H1 : ?M::2 ⊢ ?M::3 ∧ ?M::4 ≺ ?M::1
+                    Destruct/Decompose
+                     ⊢ Π H1 : ?M::2, ?M::3 ∧ ?M::4 ≺ Π _ : ?M::0, ?M::1
+                        (line: 20: pos: 18) Type of argument 3 must be convertible to the expected type in the application of
+                            Discharge::explicit
+                        with arguments:
+                            ?M::0
+                            ?M::1
+                            λ H1 : ?M::2, Conj H1 (Conjunct1 H)
+                    Assignment
+                    H1 : ?M::2 ⊢ a ≺ ?M::4
+                        Substitution
+                        H1 : ?M::2 ⊢ ?M::5 ≺ ?M::4
+                            (line: 20: pos: 37) Type of argument 4 must be convertible to the expected type in the application of
+                                Conj::explicit
+                            with arguments:
+                                ?M::3
+                                ?M::4
+                                H1
+                                Conjunct1 H
+                            Assignment
+                            H1 : ?M::2 ⊢ a ≈ ?M::5
+                                Destruct/Decompose
+                                H1 : ?M::2 ⊢ a ∧ b ≺ ?M::5 ∧ ?M::6
+                                    (line: 20: pos: 45) Type of argument 3 must be convertible to the expected type in the application of
+                                        Conjunct1::explicit
+                                    with arguments:
+                                        ?M::5
+                                        ?M::6
+                                        H
 Failed to solve
  ⊢ b ≈ a
     Substitution