diff --git a/src/library/elaborator/elaborator.cpp b/src/library/elaborator/elaborator.cpp
index c348036f89..2de1d48f62 100644
--- a/src/library/elaborator/elaborator.cpp
+++ b/src/library/elaborator/elaborator.cpp
@@ -145,6 +145,8 @@ class elaborator::imp {
     unsigned                                 m_next_id;
     justification                            m_conflict;
     bool                                     m_first;
+    level                                    m_U; // universe U used for builtin kernel axioms
+    level                                    m_M; // universe M
 
     // options
     bool                                     m_use_justifications;
@@ -1031,9 +1033,17 @@ class elaborator::imp {
                 expr choices[5] = { Bool, Type(), Type(level() + 1), TypeM, TypeU };
                 push_active(mk_choice_constraint(get_context(c), b, 5, choices, new_jst));
                 return true;
+            } else if (m_env->is_ge(ty_level(a), m_U)) {
+                expr choices[2] = { a, Type(ty_level(a) + 1) };
+                push_active(mk_choice_constraint(get_context(c), b, 2, choices, new_jst));
+                return true;
+            } else if (m_env->is_ge(ty_level(a), m_M)) {
+                expr choices[3] = { a, Type(ty_level(a) + 1), TypeU };
+                push_active(mk_choice_constraint(get_context(c), b, 3, choices, new_jst));
+                return true;
             } else {
-                expr choices[5] = { a, Type(ty_level(a) + 1), Type(ty_level(a) + 2), TypeM, TypeU };
-                push_active(mk_choice_constraint(get_context(c), b, 5, choices, new_jst));
+                expr choices[4] = { a, Type(ty_level(a) + 1), TypeM, TypeU };
+                push_active(mk_choice_constraint(get_context(c), b, 4, choices, new_jst));
                 return true;
             }
         } else {
@@ -1534,6 +1544,8 @@ public:
         set_options(opts);
         m_next_id     = 0;
         m_first       = true;
+        m_U           = m_env->get_uvar("U");
+        m_M           = m_env->get_uvar("M");
         // display(std::cout);
     }
 
diff --git a/tests/lean/elab1.lean.expected.out b/tests/lean/elab1.lean.expected.out
index 4f9fd3f433..82243bfc77 100644
--- a/tests/lean/elab1.lean.expected.out
+++ b/tests/lean/elab1.lean.expected.out
@@ -207,8 +207,7 @@ Failed to solve
             Bool
             Bool
     Failed to solve
-     ⊢
-    (?M::0 ≈ Type) ⊕ (?M::0 ≈ (Type 1)) ⊕ (?M::0 ≈ (Type 2)) ⊕ (?M::0 ≈ (Type M)) ⊕ (?M::0 ≈ (Type U))
+     ⊢ (?M::0 ≈ Type) ⊕ (?M::0 ≈ (Type 1)) ⊕ (?M::0 ≈ (Type M)) ⊕ (?M::0 ≈ (Type U))
         Destruct/Decompose
          ⊢ Type ≺ ?M::0
             (line: 24: pos: 6) Type of argument 2 must be convertible to the expected type in the application of
@@ -239,17 +238,6 @@ Failed to solve
                 Assignment
                  ⊢ ?M::1 ≈ Type
                     Assumption 0
-        Failed to solve
-         ⊢ (Type 3) ≺ Type
-            Substitution
-             ⊢ (Type 3) ≺ ?M::1
-                Propagate type, ?M::0 : ?M::1
-                    Assignment
-                     ⊢ ?M::0 ≈ (Type 2)
-                        Assumption 3
-                Assignment
-                 ⊢ ?M::1 ≈ Type
-                    Assumption 0
         Failed to solve
          ⊢ (Type M+1) ≺ Type
             Substitution
@@ -257,7 +245,7 @@ Failed to solve
                 Propagate type, ?M::0 : ?M::1
                     Assignment
                      ⊢ ?M::0 ≈ (Type M)
-                        Assumption 4
+                        Assumption 3
                 Assignment
                  ⊢ ?M::1 ≈ Type
                     Assumption 0
@@ -268,13 +256,12 @@ Failed to solve
                 Propagate type, ?M::0 : ?M::1
                     Assignment
                      ⊢ ?M::0 ≈ (Type U)
-                        Assumption 5
+                        Assumption 4
                 Assignment
                  ⊢ ?M::1 ≈ Type
                     Assumption 0
     Failed to solve
-     ⊢
-    (?M::0 ≈ Type) ⊕ (?M::0 ≈ (Type 1)) ⊕ (?M::0 ≈ (Type 2)) ⊕ (?M::0 ≈ (Type M)) ⊕ (?M::0 ≈ (Type U))
+     ⊢ (?M::0 ≈ Type) ⊕ (?M::0 ≈ (Type 1)) ⊕ (?M::0 ≈ (Type M)) ⊕ (?M::0 ≈ (Type U))
         Destruct/Decompose
          ⊢ Type ≺ ?M::0
             (line: 24: pos: 6) Type of argument 2 must be convertible to the expected type in the application of
@@ -290,10 +277,10 @@ Failed to solve
                 Propagate type, ?M::0 : ?M::1
                     Assignment
                      ⊢ ?M::0 ≈ Type
-                        Assumption 7
+                        Assumption 6
                 Assignment
                  ⊢ ?M::1 ≈ Bool
-                    Assumption 6
+                    Assumption 5
         Failed to solve
          ⊢ (Type 2) ≺ Bool
             Substitution
@@ -301,21 +288,10 @@ Failed to solve
                 Propagate type, ?M::0 : ?M::1
                     Assignment
                      ⊢ ?M::0 ≈ (Type 1)
-                        Assumption 8
+                        Assumption 7
                 Assignment
                  ⊢ ?M::1 ≈ Bool
-                    Assumption 6
-        Failed to solve
-         ⊢ (Type 3) ≺ Bool
-            Substitution
-             ⊢ (Type 3) ≺ ?M::1
-                Propagate type, ?M::0 : ?M::1
-                    Assignment
-                     ⊢ ?M::0 ≈ (Type 2)
-                        Assumption 9
-                Assignment
-                 ⊢ ?M::1 ≈ Bool
-                    Assumption 6
+                    Assumption 5
         Failed to solve
          ⊢ (Type M+1) ≺ Bool
             Substitution
@@ -323,10 +299,10 @@ Failed to solve
                 Propagate type, ?M::0 : ?M::1
                     Assignment
                      ⊢ ?M::0 ≈ (Type M)
-                        Assumption 10
+                        Assumption 8
                 Assignment
                  ⊢ ?M::1 ≈ Bool
-                    Assumption 6
+                    Assumption 5
         Failed to solve
          ⊢ (Type U+1) ≺ Bool
             Substitution
@@ -334,10 +310,10 @@ Failed to solve
                 Propagate type, ?M::0 : ?M::1
                     Assignment
                      ⊢ ?M::0 ≈ (Type U)
-                        Assumption 11
+                        Assumption 9
                 Assignment
                  ⊢ ?M::1 ≈ Bool
-                    Assumption 6
+                    Assumption 5
 Failed to solve
 a : Bool, b : Bool, H : ?M::2, H_a : ?M::6 ⊢ (a ⇒ b) ⇒ a ≺ a
     Substitution
diff --git a/tests/lean/tactic7.lean b/tests/lean/tactic7.lean
deleted file mode 100644
index 50334e64f4..0000000000
--- a/tests/lean/tactic7.lean
+++ /dev/null
@@ -1,50 +0,0 @@
-Variable Eq      {A : (Type U+1)} (a b : A) : Bool
-Infix 50 === : Eq
-Axiom EqSubst {A : (Type U+1)} {a b : A} (P : A -> Bool) (H1 : P a) (H2 : a === b) : P b
-Axiom EqRefl  {A : (Type U+1)} (a : A) : a === a
-Theorem EqSymm {A : (Type U+1)} {a b : A} (H : a === b) : b === a :=
-        EqSubst (fun x, x === a) (EqRefl a) H
-Theorem EqTrans {A : (Type U+1)} {a b c : A} (H1 : a === b) (H2 : b === c) : a === c :=
-        EqSubst (fun x, a === x) H1 H2
-Theorem EqCongr {A B : (Type U+1)} (f : A -> B) {a b : A} (H : a === b) : (f a) === (f b) :=
-        EqSubst (fun x, (f a) === (f x)) (EqRefl (f a)) H
-Theorem EqCongr1 {A : (Type U+1)} {B : A -> (Type U+1)} {f g : Pi x : A, B x} (a : A) (H : f === g) : (f a) === (g a) :=
-        EqSubst (fun h : (Pi x : A, B x), (f a) === (h a)) (EqRefl (f a)) H
-Axiom ProofIrrelevance (P : Bool) (pr1 pr2 : P) : pr1 === pr2
-Axiom EqCast {A B : (Type U)} (H : A === B) (a : A) : B
-Axiom EqCastHom {A B : (Type U)} {a1 a2 : A} (HAB : A === B) (H : a1 === a2) : (EqCast HAB a1) === (EqCast HAB a2)
-Axiom EqCastRefl {A : (Type U)} (a : A) : (EqCast (EqRefl A) a) === a
-
-Variable Vector : (Type U) -> Nat -> (Type U)
-Variable empty {A : (Type U)} : Vector A 0
-Variable append {A : (Type U)} {m n : Nat} (v1 : Vector A m) (v2 : Vector A n) : Vector A (m + n)
-Axiom Plus0 (n : Nat) : (n + 0) === n
-Theorem VectorPlus0 (A : (Type U)) (n : Nat) : (Vector A (n + 0)) === (Vector A n) :=
-        EqSubst (fun x : Nat, (Vector A x) === (Vector A n))
-                (EqRefl (Vector A n))
-                (EqSymm (Plus0 n))
-SetOption pp::implicit true
-(* Check fun (A : Type) (n : Nat), VectorPlus0 A n *)
-Axiom AppendNil {A : Type} {n : Nat} (v : Vector A n) : (EqCast (VectorPlus0 A n) (append v empty)) === v
-
-Variable List : (Type U) -> (Type U).
-Variables A B : (Type U)
-Axiom H1 : A === B.
-Theorem LAB : (List A) === (List B) :=
-        EqCongr List H1
-Variable l1 : List A
-Variable l2 : List B
-Variable H2 : (EqCast LAB l1) == l2
-
-
-(*
-Theorem EqCastInv {A B : (Type U)} (H : A === B) (a : A) : (EqCast (EqSymm H) (EqCast H a)) === a :=
-*)
-
-(*
-Variable ReflCast : Pi (A : (Type U)) (a : A) (H : Eq (Type U) A A), Eq A (Casting A A H a) a
-Theorem AppEq (A : (Type U)) (B : A -> (Type U)) (a b : A) (H : Eq A a b) : (Eq (Type U) (B b) (B a)) :=
-        EqCongr A (Type U) B b a (EqSymm A a b H)
-Theorem EqCongr2 (A : (Type U)) (B : A -> (Type U)) (f : Pi x : A, B x) (a b : A) (H : Eq A a b) : Eq (B a) (f a) (Casting (B b) (B a) (AppEq A B a b H) (f a)) (f b) :=
-        EqSubst (B a) a b (fun x : A, Eq (B a) (f a) (Casting (B x) (B a) (AppEq A B a b H) (f a)) (f x)
-*)
\ No newline at end of file
diff --git a/tests/lean/tactic7.lean.expected.out b/tests/lean/tactic7.lean.expected.out
deleted file mode 100644
index 99a5c5a6b9..0000000000
--- a/tests/lean/tactic7.lean.expected.out
+++ /dev/null
@@ -1,28 +0,0 @@
-  Set: pp::colors
-  Set: pp::unicode
-  Assumed: Eq
-  Assumed: EqSubst
-  Assumed: EqRefl
-  Proved: EqSymm
-  Proved: EqTrans
-  Proved: EqCongr
-  Proved: EqCongr1
-  Assumed: ProofIrrelevance
-  Assumed: EqCast
-  Assumed: EqCastHom
-  Assumed: EqCastRefl
-  Assumed: Vector
-  Assumed: empty
-  Assumed: append
-  Assumed: Plus0
-  Proved: VectorPlus0
-  Set: lean::pp::implicit
-  Assumed: AppendNil
-  Assumed: List
-  Assumed: A
-  Assumed: B
-  Assumed: H1
-  Proved: LAB
-  Assumed: l1
-  Assumed: l2
-  Assumed: H2