diff --git a/src/tests/kernel/metavar.cpp b/src/tests/kernel/metavar.cpp
index d1934cd7e..59f2bb7d7 100644
--- a/src/tests/kernel/metavar.cpp
+++ b/src/tests/kernel/metavar.cpp
@@ -14,19 +14,6 @@ Author: Leonardo de Moura
 #include "kernel/metavar.h"
 #include "kernel/instantiate.h"
 #include "kernel/abstract.h"
-// #include "kernel/free_vars.h"
-// #include "kernel/normalizer.h"
-// #include "kernel/environment.h"
-// #include "kernel/type_checker.h"
-// #include "kernel/kernel_exception.h"
-// #include "kernel/kernel.h"
-// #include "kernel/io_state.h"
-// #include "library/printer.h"
-// #include "library/io_state_stream.h"
-// #include "library/placeholder.h"
-// #include "library/arith/arith.h"
-// #include "frontends/lean/frontend.h"
-// #include "frontends/lua/register_modules.h"
 using namespace lean;
 
 void collect_assumptions(justification const & j, buffer<unsigned> & r) {
@@ -117,608 +104,41 @@ static void tst2() {
     check_assumptions(p1.second, {1, 2});
     lean_assert(check_assumptions(s.get_assignment(m1)->second, {1}));
     lean_assert(p1.first == g(f(g(a))));
-    auto p2 = s.d_instantiate_metavars(g(m1));
+    auto p2 = s.d_instantiate_metavars(g(m1, m3));
     check_assumptions(p2.second, {1, 2});
+    std::cout << p2.first << "\n";
     std::cout << s << "\n";
     lean_assert(check_assumptions(s.get_assignment(m1)->second, {1, 2}));
-}
-
-#if 0
-static void tst2() {
-    metavar_env menv;
-    expr f = Const("f");
-    expr g = Const("g");
-    expr h = Const("h");
-    expr a = Const("a");
-    expr T = Const("T");
-    expr m1 = menv->mk_metavar(context({{"x", T}, {"y", T}}));
-    expr m2 = menv->mk_metavar(context({{"x", T}, {"y", T}}));
-    // move m1 to a different context, and store new metavariable + context in m11
-    std::cout << "---------------------\n";
-    expr m11 = add_inst(m1, 0, f(a, m2));
-    std::cout << m11 << "\n";
-    menv->assign(m1, f(Var(0)));
-    std::cout << menv->instantiate_metavars(m11) << "\n";
-    menv->assign(m2, g(a, Var(1)));
-    std::cout << menv->instantiate_metavars(h(m11)) << "\n";
-    lean_assert_eq(menv->instantiate_metavars(h(m11)), h(f(f(a, g(a, Var(1))))));
+    lean_assert(p2.first == g(f(g(a)), m3));
+    s.assign(m3, f(m1, m2), mk_assumption_justification(3));
+    auto p3 = s.instantiate_metavars(g(m1, m3));
+    lean_assert(check_assumptions(p3.second, {1, 2, 3}));
+    std::cout << p3.first << "\n";
+    std::cout << p3.second << "\n";
+    std::cout << s << "\n";
+    lean_assert_eq(p3.first, g(f(g(a)), f(f(g(a)), g(a))));
 }
 
 static void tst3() {
-    metavar_env menv;
-    expr f = Const("f");
-    expr g = Const("g");
-    expr h = Const("h");
-    expr a = Const("a");
-    expr x = Const("x");
-    expr T = Const("T");
-    expr m1 = menv->mk_metavar(context({{"x", T}, {"y", T}, {"z", T}}));
-    expr F = Fun({x, T}, f(m1, x));
-    menv->assign(m1, h(Var(0), Var(2)));
-    std::cout << instantiate(abst_body(F), g(a)) << "\n";
-    lean_assert(menv->instantiate_metavars(instantiate(abst_body(F), g(a))) == f(h(g(a), Var(1)), g(a)));
-    std::cout << instantiate(menv->instantiate_metavars(abst_body(F)), g(a)) << "\n";
-    lean_assert(instantiate(menv->instantiate_metavars(abst_body(F)), g(a)) ==
-                menv->instantiate_metavars(instantiate(abst_body(F), g(a))));
-}
-
-static void tst4() {
-    metavar_env menv;
-    expr f = Const("f");
-    expr g = Const("g");
-    expr h = Const("h");
-    expr a = Const("a");
-    expr T = Const("T");
-    expr m1 = menv->mk_metavar(context({{"x", T}, {"y", T}}));
-    expr F = f(m1, Var(2));
-    menv->assign(m1, h(Var(1)));
-    std::cout << instantiate(F, {g(Var(0)), h(a)}) << "\n";
-    std::cout << menv->instantiate_metavars(instantiate(F, {g(Var(0)), h(a)})) << "\n";
-}
-
-static void tst5() {
-    return;
-}
-
-static void tst6() {
-    expr N  = Const("N");
+    expr m1 = mk_metavar("m1", Bool >> (Bool >> Bool));
+    substitution s;
     expr f  = Const("f");
+    expr g  = Const("g");
     expr x  = Const("x");
     expr y  = Const("y");
     expr a  = Const("a");
-    expr g  = Const("g");
-    expr h  = Const("h");
-    metavar_env menv;
-    expr T  = Const("T");
-    expr m1 = menv->mk_metavar(context({{"x1", T}, {"x2", T}, {"x3", T}, {"x4", T}}));
-    expr m2 = menv->mk_metavar(context({{"x1", T}, {"x2", T}, {"x3", T}, {"x4", T}}));
-    expr t = f(Var(0), Fun({x, N}, f(Var(1), x, Fun({y, N}, f(Var(2), x, y)))));
-    expr r = instantiate(t, g(m1, m2));
-    std::cout << r << std::endl;
-    menv->assign(m2, Var(2));
-    r = menv->instantiate_metavars(r);
-    std::cout << r << std::endl;
-    menv->assign(m1, h(Var(3)));
-    r = menv->instantiate_metavars(r);
-    std::cout << r << std::endl;
-    lean_assert(r == f(g(h(Var(3)), Var(2)), Fun({x, N}, f(g(h(Var(4)), Var(3)), x, Fun({y, N}, f(g(h(Var(5)), Var(4)), x, y))))));
-}
-
-static void tst7() {
-    expr f  = Const("f");
-    expr g  = Const("g");
-    expr a  = Const("a");
-    metavar_env menv;
-    expr T  = Const("T");
-    expr m1 = menv->mk_metavar(context({{"x", T}}));
-    expr t  = f(m1, Var(0));
-    expr r = instantiate(t, a);
-    menv->assign(m1, g(Var(0)));
-    r = menv->instantiate_metavars(r);
-    std::cout << r << std::endl;
-    lean_assert(r == f(g(a), a));
-}
-
-static void tst8() {
-    expr f  = Const("f");
-    expr g  = Const("g");
-    expr a  = Const("a");
-    metavar_env menv;
-    expr T  = Const("T");
-    expr m1 = menv->mk_metavar(context({{"x1", T}, {"x2", T}, {"x3", T}, {"x4", T}}));
-    expr t  = f(m1, Var(0), Var(2));
-    expr r = instantiate(t, a);
-    menv->assign(m1, g(Var(0), Var(1)));
-    r = menv->instantiate_metavars(r);
-    std::cout << r << std::endl;
-    lean_assert(r == f(g(a, Var(0)), a, Var(1)));
-}
-
-static void tst9() {
-    expr f  = Const("f");
-    expr g  = Const("g");
-    expr a  = Const("a");
-    metavar_env menv;
-    expr T  = Const("T");
-    expr m1 = menv->mk_metavar(context({{"x1", T}, {"x2", T}, {"x3", T}, {"x4", T}}));
-    expr t  = f(m1, Var(1), Var(2));
-    expr r  = lift_free_vars(t, 1, 2);
-    std::cout << r << std::endl;
-    r = instantiate(r, a);
-    std::cout << r << std::endl;
-    menv->assign(m1, g(Var(0), Var(1)));
-    r = menv->instantiate_metavars(r);
-    std::cout << r << std::endl;
-    lean_assert(r == f(g(a, Var(2)), Var(2), Var(3)));
-}
-
-static void tst10() {
-    expr N  = Const("N");
-    expr f  = Const("f");
-    expr x  = Const("x");
-    expr y  = Const("y");
-    expr a  = Const("a");
-    expr g  = Const("g");
-    expr h  = Const("h");
-    metavar_env menv;
-    expr T  = Const("T");
-    expr m1 = menv->mk_metavar(context({{"x1", T}, {"x2", T}, {"x3", T}, {"x4", T}}));
-    expr m2 = menv->mk_metavar(context({{"x1", T}, {"x2", T}, {"x3", T}, {"x4", T}}));
-    expr t = f(Var(0), Fun({x, N}, f(Var(1), Var(2), x, Fun({y, N}, f(Var(2), x, y)))));
-    expr r = instantiate(t, g(m1));
-    std::cout << r << std::endl;
-    r = instantiate(r, h(m2));
-    std::cout << r << std::endl;
-    menv->assign(m1, f(Var(0)));
-    menv->assign(m2, Var(2));
-    r = menv->instantiate_metavars(r);
-    std::cout << r << std::endl;
-    lean_assert(r == f(g(f(h(Var(2)))), Fun({x, N}, f(g(f(h(Var(3)))), h(Var(3)), x, Fun({y, N}, f(g(f(h(Var(4)))), x, y))))));
-}
-
-static void tst11() {
-    metavar_env menv;
-    unsigned t1 = menv->get_timestamp();
-    expr m = menv->mk_metavar();
-    unsigned t2 = menv->get_timestamp();
-    lean_assert(t2 > t1);
-    lean_assert(!menv->is_assigned(m));
-    lean_assert(menv->get_timestamp() == t2);
-    menv->assign(m, Const("a"));
-    lean_assert(menv->get_timestamp() > t2);
-}
-
-static void tst12() {
-    metavar_env menv;
-    expr T  = Const("T");
-    expr m = menv->mk_metavar(context({{"x1", T}, {"x2", T}}));
-    expr f = Const("f");
-    std::cout << instantiate(f(m), {Var(0), Var(1)}) << "\n";
-    std::cout << instantiate(f(m), {Var(1), Var(0)}) << "\n";
-}
-
-static void tst13() {
-    environment env;
-    metavar_env menv;
-    expr T  = Const("T");
-    expr m = menv->mk_metavar(context({{"x", T}}));
-    env->add_var("N", Type());
-    expr N = Const("N");
-    env->add_var("f", N >> N);
-    expr f = Const("f");
-    env->add_var("a", N);
-    expr a = Const("a");
-    expr x = Const("x");
-    expr F = Fun({x, N}, f(m))(a);
-    normalizer norm(env);
-    std::cout << norm(F) << "\n";
-    menv->assign(m, Var(0));
-    std::cout << norm(menv->instantiate_metavars(F)) << "\n";
-    lean_assert(norm(menv->instantiate_metavars(F)) ==
-                menv->instantiate_metavars(norm(F)));
-}
-
-static void tst14() {
-    environment env;
-    metavar_env menv;
-    expr T  = Const("T");
-    expr m1 = menv->mk_metavar(context({{"x1", T}, {"x2", T}, {"x3", T}, {"x4", T}, {"x5", T}}));
-    expr m2 = menv->mk_metavar(context({{"x1", T}, {"x2", T}, {"x3", T}, {"x4", T}, {"x5", T}}));
-    expr N = Const("N");
-    expr f = Const("f");
-    expr h = Const("h");
-    expr a = Const("a");
-    expr b = Const("b");
-    expr x = Const("x");
-    expr y = Const("y");
-    env->add_var("h", Pi({N, Type()}, N >> (N >> N)));
-    expr F1 = Fun({{N, Type()}, {a, N}, {f, N >> N}},
-                  (Fun({{x, N}, {y, N}}, mk_eq(N, f(m1), y)))(a));
-    metavar_env menv2 = menv.copy();
-    menv2->assign(m1, h(Var(4), Var(1), Var(3)));
-    normalizer norm(env);
-    env->add_var("M", Type());
-    expr M = Const("M");
-    std::cout << norm(F1) << "\n";
-    std::cout << menv2->instantiate_metavars(norm(F1)) << "\n";
-    std::cout << menv2->instantiate_metavars(F1) << "\n";
-    std::cout << norm(menv2->instantiate_metavars(F1)) << "\n";
-    lean_assert(menv2->instantiate_metavars(norm(F1)) ==
-                norm(menv2->instantiate_metavars(F1)));
-}
-
-static void tst15() {
-    environment env;
-    metavar_env menv;
-    normalizer  norm(env);
-    expr T  = Const("T");
-    expr m1 = menv->mk_metavar(context({{"x1", T}, {"x2", T}, {"x3", T}}));
-    expr f = Const("f");
-    expr x = Const("x");
-    expr y = Const("y");
-    expr z = Const("z");
-    expr N = Const("N");
-    env->add_var("N", Type());
-    env->add_var("f", Type() >> Type());
-    expr F = Fun({z, Type()}, Fun({{x, Type()}, {y, Type()}}, f(m1))(N, N));
-    menv->assign(m1, Var(2));
-    std::cout << norm(F) << "\n";
-    std::cout << menv->instantiate_metavars(norm(F)) << "\n";
-    std::cout << norm(menv->instantiate_metavars(F)) << "\n";
-    lean_assert(menv->instantiate_metavars(norm(F)) ==
-                norm(menv->instantiate_metavars(F)));
-}
-
-static void tst16() {
-    environment env;
-    metavar_env menv;
-    normalizer  norm(env);
-    context ctx;
-    ctx = extend(ctx, "w", Type());
-    expr T  = Const("T");
-    expr m1 = menv->mk_metavar(context({{"x1", T}, {"x2", T}, {"x3", T}, {"x4", T}, {"x5", T}}));
-    expr f = Const("f");
-    expr x = Const("x");
-    expr y = Const("y");
-    expr z = Const("z");
-    expr N = Const("N");
-    env->add_var("N", Type());
-    expr F = Fun({z, Type()}, Fun({{x, Type()}, {y, Type()}}, m1)(N, N));
-    menv->assign(m1, Var(3));
-    std::cout << norm(F, ctx) << "\n";
-    std::cout << menv->instantiate_metavars(norm(F, ctx)) << "\n";
-    std::cout << norm(menv->instantiate_metavars(F), ctx) << "\n";
-}
-
-static void tst17() {
-    environment env;
-    metavar_env menv;
-    normalizer  norm(env);
-    context ctx;
-    ctx = extend(ctx, "w1", Type());
-    ctx = extend(ctx, "w2", Type());
-    ctx = extend(ctx, "w3", Type());
-    ctx = extend(ctx, "w4", Type());
-    expr T  = Const("T");
-    expr m1 = menv->mk_metavar(context({{"x1", T}, {"x2", T}, {"x3", T}, {"x4", T}}));
-    expr f = Const("f");
-    expr x = Const("x");
-    expr y = Const("y");
-    expr z = Const("z");
-    expr N = Const("N");
-    env->add_var("N", Type());
-    expr F = Fun({z, Type()}, Fun({{x, Type()}, {y, Type()}}, m1)(N, N));
-    metavar_env menv2 = menv.copy();
-    menv->assign(m1, Var(3));
-    std::cout << norm(F, ctx) << "\n";
-    std::cout << menv->instantiate_metavars(norm(F, ctx)) << "\n";
-    std::cout << norm(menv->instantiate_metavars(F), ctx) << "\n";
-    F = Fun({z, Type()}, Fun({{x, Type()}, {y, Type()}, {x, Type()}, {y, Type()}, {x, Type()}}, m1)(N, N, N, N, N));
-    lean_assert(menv->instantiate_metavars(norm(F, ctx)) ==
-                norm(menv->instantiate_metavars(F), ctx));
-    std::cout << "----------------------\n";
-    menv2->assign(m1, Var(8));
-    std::cout << norm(F, ctx) << "\n";
-    std::cout << menv2->instantiate_metavars(norm(F, ctx)) << "\n";
-    std::cout << norm(menv2->instantiate_metavars(F), ctx) << "\n";
-    lean_assert(menv2->instantiate_metavars(norm(F, ctx)) ==
-                norm(menv2->instantiate_metavars(F), ctx));
-}
-
-static void tst18() {
-    environment env;
-    metavar_env menv;
-    normalizer  norm(env);
-    expr f = Const("f");
-    expr g = Const("g");
-    expr h = Const("h");
-    expr x = Const("x");
-    expr y = Const("y");
-    expr z = Const("z");
-    expr N = Const("N");
-    expr a = Const("a");
-    context ctx({{"x1", N}});
-    env->add_var("N", Type());
-    env->add_var("a", N);
-    env->add_var("g", N >> N);
-    env->add_var("h", N >> (N >> N));
-    expr m1 = menv->mk_metavar(context({{"x1", N}, {"z", Type()}, {"f", N >> N}, {"y", Type()}}));
-    expr m2 = menv->mk_metavar(context({{"x1", N}, {"z", Type()}, {"x", N}}));
-    expr F = Fun({z, Type()}, Fun({{f, N >> N}, {y, Type()}}, m1)(Fun({x, N}, g(z, x, m2)), N));
-    std::cout << norm(F, ctx) << "\n";
-    metavar_env menv2 = menv.copy();
-    menv2->assign(m1, Var(1));
-    menv2->assign(m2, h(Var(2), Var(1)));
-    std::cout << menv2->instantiate_metavars(norm(F, ctx)) << "\n";
-    std::cout << menv2->instantiate_metavars(F) << "\n";
-    lean_assert_eq(menv2->instantiate_metavars(norm(F, ctx, menv2)),
-                   norm(menv2->instantiate_metavars(F), ctx, menv2));
-    std::cout << "norm(F...): " << norm(F, ctx, menv2) << "\n";
-    lean_assert(menv2->is_assigned(m1));
-    lean_assert(menv2->is_assigned(m2));
-    lean_assert_eq(menv2->instantiate_metavars(norm(F, ctx, menv2)),
-                   Fun({{z, Type()}, {x, N}}, g(z, x, h(Var(2), z))));
-}
-
-static void tst19() {
-    environment env;
-    metavar_env menv;
-    normalizer  norm(env);
-    context ctx;
-    ctx = extend(ctx, "w1", Type());
-    ctx = extend(ctx, "w2", Type());
-    expr x  = Const("x");
-    expr y  = Const("y");
-    expr N  = Const("N");
-    expr m1 = menv->mk_metavar(context({{"N", Type()}, {"x", N}, {"y", N}}));
-    expr F  = Fun({{N, Type()}, {x, N}, {y, N}}, m1);
-    std::cout << norm(F) << "\n";
-    std::cout << norm(F, ctx) << "\n";
-    lean_assert_eq(norm(F, context(), menv), F);
-    lean_assert_eq(norm(F, ctx, menv), F);
-}
-
-static void tst20() {
-    environment env;
-    metavar_env menv;
-    normalizer  norm(env);
-    context ctx;
-    ctx = extend(ctx, "w1", Type());
-    ctx = extend(ctx, "w2", Type());
-    expr x = Const("x");
-    expr y = Const("y");
-    expr z = Const("z");
-    expr N = Const("N");
-    expr a = Const("a");
-    expr b = Const("b");
-    expr m1 = menv->mk_metavar(context({{"x", N}, {"y", N}, {"z", N}, {"x", N}, {"y", N}}));
-    env->add_var("N", Type());
-    env->add_var("a", N);
-    env->add_var("b", N);
-    expr F = Fun({{x, N}, {y, N}, {z, N}}, Fun({{x, N}, {y, N}}, m1)(a, b));
-    std::cout << norm(F) << "\n";
-    std::cout << norm(F, ctx) << "\n";
-}
-
-static void tst21() {
-    metavar_env menv;
-    expr m1 = menv->mk_metavar();
-    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_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()
-
-static void tst22() {
-    metavar_env menv;
-    expr f = Const("f");
-    expr x = Const("x");
-    expr N = Const("N");
-    expr F = f(Fun({x, N}, f(_, x)), _);
-    std::cout << F << "\n";
-    std::cout << replace_placeholders_with_metavars(F, menv) << "\n";
-}
-
-static void tst23() {
-    environment env;
-    metavar_env menv;
-    type_checker checker(env);
-    expr N  = Const("N");
-    expr f  = Const("f");
-    expr a  = Const("a");
-    env->add_var("N", Type());
-    env->add_var("f", N >> (N >> N));
-    env->add_var("a", N);
-    expr x  = Const("x");
-    expr F0 = f(Fun({x, N}, f(_, x))(a), _);
-    expr F1 = replace_placeholders_with_metavars(F0, menv);
-    buffer<unification_constraint> up;
-    std::cout << F1 << "\n";
-    try {
-        std::cout << checker.check(F1, context(), menv, up) << "\n";
-    } catch (kernel_exception & ex) {
-        formatter fmt = mk_simple_formatter();
-        io_state st(options(), fmt);
-        regular(st) << ex << "\n";
-    }
-    std::cout << up << "\n";
-}
-
-static void tst24() {
-    metavar_env menv;
-    expr m1 = menv->mk_metavar();
-    expr m2 = menv->mk_metavar();
-    expr f  = Const("f");
-    expr a  = Const("a");
-    menv->assign(m1, f(m2));
-    menv->assign(m2, a);
-    lean_assert(menv->instantiate_metavars(f(m1)) == f(f(a)));
-    std::cout << menv->instantiate_metavars(f(m1)) << "\n";
-}
-
-static void tst25() {
-    environment env;
-    metavar_env menv;
-    buffer<unification_constraint> up;
-    type_checker checker(env);
-    expr N = Const("N");
-    expr a = Const("a");
-    expr b = Const("b");
-    env->add_var("N", Type());
-    env->add_var("a", N);
-    env->add_var("b", N);
-    expr m = menv->mk_metavar();
-    expr F = m(a, b);
-    std::cout << checker.check(F, context(), menv, up) << "\n";
-    std::cout << menv << "\n";
-    std::cout << up << "\n";
-}
-
-static void tst26() {
-    /*
-      Encoding the following problem
-
-      Variable list : Type -> Type
-      Variable nil  {A : Type} : list A
-      Variable cons {A : Type} (head : A) (tail : list A) : list A
-      Variables a b : Int
-      Variables n m : Nat
-      Definition l2 : list Int := cons a (cons n (cons b nil))
-    */
-    std::cout << "\ntst26\n";
-    environment  env;
-    init_test_frontend(env);
-    metavar_env menv;
-    buffer<unification_constraint> up;
-    type_checker checker(env);
-    expr list = Const("list");
-    expr nil  = Const("nil");
-    expr cons = Const("cons");
-    expr A    = Const("A");
-    env->add_var("list", Type() >> Type());
-    env->add_var("nil", Pi({A, Type()}, list(A)));
-    env->add_var("cons", Pi({A, Type()}, A >> (list(A) >> list(A))));
-    env->add_var("a", Int);
-    env->add_var("b", Int);
-    env->add_var("n", Nat);
-    env->add_var("m", Nat);
-    expr a  = Const("a");
     expr b  = Const("b");
-    expr n  = Const("n");
-    expr m  = Const("m");
-    expr m1 = menv->mk_metavar();
-    expr m2 = menv->mk_metavar();
-    expr m3 = menv->mk_metavar();
-    expr A1 = menv->mk_metavar();
-    expr A2 = menv->mk_metavar();
-    expr A3 = menv->mk_metavar();
-    expr A4 = menv->mk_metavar();
-    expr F  = cons(A1, m1(a), cons(A2, m2(n), cons(A3, m3(b), nil(A4))));
-    std::cout << F << "\n";
-    std::cout << checker.check(F, context(), menv, up) << "\n";
-    std::cout << menv << "\n";
-    std::cout << up << "\n";
+    s.assign(m1, Fun({{x, Bool}, {y, Bool}}, f(y, x)));
+    lean_assert_eq(s.instantiate_metavars(m1(a, b, g(a))).first, f(b, a, g(a)));
+    lean_assert_eq(s.instantiate_metavars(m1(a)).first, Fun({y, Bool}, f(y, a)));
+    lean_assert_eq(s.instantiate_metavars(m1(a, b)).first, f(b, a));
+    std::cout << s.instantiate_metavars(m1(a, b, g(a))).first << "\n";
 }
 
-static void tst27() {
-    /*
-      Variable f {A : Type} (a b : A) : Bool
-      Variable a : Int
-      Variable b : Real
-      Definition tst : Bool := (fun x y, f x y) a b
-    */
-    std::cout << "\ntst27\n";
-    environment  env;
-    init_test_frontend(env);
-    metavar_env menv;
-    buffer<unification_constraint> up;
-    type_checker checker(env);
-    expr A    = Const("A");
-    expr f    = Const("f");
-    expr a    = Const("a");
-    expr b    = Const("b");
-    expr x    = Const("x");
-    expr y    = Const("y");
-    env->add_var("f", Pi({A, Type()}, A >> (A >> Bool)));
-    env->add_var("a", Int);
-    env->add_var("b", Real);
-    expr T1 = menv->mk_metavar();
-    expr T2 = menv->mk_metavar(context({{"x", T1}}));
-    expr A1 = menv->mk_metavar(context({{"x", T1}, {"y", T2}}));
-    expr m1 = menv->mk_metavar(context({{"x", T1}, {"y", T2}}));
-    expr m2 = menv->mk_metavar(context({{"x", T1}, {"y", T2}}));
-    expr F = Fun({{x, T1}, {y, T2}}, f(A1, x, y))(m1(a), m2(b));
-    std::cout << F << "\n";
-    std::cout << checker.check(F, context(), menv, up) << "\n";
-    std::cout << menv << "\n";
-    std::cout << up << "\n";
-}
-
-static void tst28() {
-    metavar_env menv;
-    expr f = Const("f");
-    expr a = Const("a");
-    expr m1 = menv->mk_metavar();
-    lean_assert(add_inst(m1, 0, f(a), menv) == m1);
-    lean_assert(add_inst(m1, 1, f(a), menv) == m1);
-    lean_assert(add_lift(m1, 0, 2, menv) == m1);
-    lean_assert(add_lift(m1, 1, 2, menv) == m1);
-    expr m2 = menv->mk_metavar(context({{"x", Bool}, {"y", Bool}}));
-    lean_assert(add_inst(m2, 0, f(a), menv) != m2);
-    lean_assert(add_inst(m2, 0, f(a), menv) == add_inst(m2, 0, f(a)));
-    lean_assert(add_inst(m2, 1, f(a), menv) != m2);
-    lean_assert(add_inst(m2, 2, f(a), menv) == m2);
-    lean_assert(add_lift(m2, 0, 2, menv) != m2);
-    lean_assert(add_lift(m2, 0, 2, menv) == add_lift(m2, 0, 2));
-    lean_assert(add_lift(m2, 1, 2, menv) != m2);
-    lean_assert(add_lift(m2, 2, 2, menv) == m2);
-    lean_assert(add_lift(m2, 2, 2, menv) != add_lift(m2, 2, 2));
-}
-#endif
-
 int main() {
     save_stack_info();
     tst1();
     tst2();
-#if 0
     tst3();
-    tst4();
-    tst5();
-    tst6();
-    tst7();
-    tst8();
-    tst9();
-    tst10();
-    tst11();
-    tst12();
-    tst13();
-    tst14();
-    tst15();
-    tst16();
-    tst17();
-    tst18();
-    tst19();
-    tst20();
-    tst21();
-    tst22();
-    tst23();
-    tst24();
-    tst25();
-    tst26();
-    tst27();
-    tst28();
-#endif
     return has_violations() ? 1 : 0;
 }