diff --git a/src/builtin/heq.lean b/src/builtin/heq.lean
index 6321f7e77..130458d27 100644
--- a/src/builtin/heq.lean
+++ b/src/builtin/heq.lean
@@ -1,75 +1,4 @@
 -- Axioms and theorems for casting and heterogenous equality
 import macros
 
--- In the following definitions the type of A and B cannot be (Type U)
--- because A = B would be @eq (Type U+1) A B, and
--- the type of eq is (∀T : (Type U), T → T → bool).
--- So, we define M a universe smaller than U.
-universe M ≥ 1
-definition TypeM := (Type M)
 
-variable cast {A B : (Type M)} : A = B → A → B
-
-axiom cast_heq {A B : (Type M)} (H : A = B) (a : A) : cast H a == a
-
-axiom hsymm {A B : (Type U)} {a : A} {b : B} : a == b → b == a
-
-axiom htrans {A B C : (Type U)} {a : A} {b : B} {c : C} : a == b → b == c → a == c
-
-axiom hcongr {A A' : (Type U)} {B : A → (Type U)} {B' : A' → (Type U)} {f : ∀ x, B x} {f' : ∀ x, B' x} {a : A} {a' : A'} :
-      f == f' → a == a' → f a == f' a'
-
-axiom hfunext {A A' : (Type M)} {B : A → (Type U)} {B' : A' → (Type U)} {f : ∀ x, B x} {f' : ∀ x, B' x} :
-      A = A' → (∀ x x', x == x' → f x == f' x') → f == f'
-
-theorem hsfunext {A : (Type M)} {B B' : A → (Type U)} {f : ∀ x, B x} {f' : ∀ x, B' x} :
-      (∀ x, f x == f' x) → f == f'
-:= λ Hb,
-     hfunext (refl A) (λ (x x' : A) (Hx : x == x'),
-                   let s1 : f x   == f' x  := Hb x,
-                       s2 : f' x  == f' x' := hcongr (hrefl f') Hx
-                   in htrans s1 s2)
-
-theorem hallext {A A' : (Type M)} {B : A → Bool} {B' : A' → Bool}
-                (Ha : A = A') (Hb : ∀ x x', x == x' → B x = B' x') : (∀ x, B x) = (∀ x, B' x)
-:= boolext
-     (assume (H : ∀ x : A, B x),
-        take x' : A', (Hb (cast (symm Ha) x') x' (cast_heq (symm Ha) x')) ◂ (H (cast (symm Ha) x')))
-     (assume (H : ∀ x' : A', B' x'),
-        take x : A, (symm (Hb x (cast Ha x) (hsymm (cast_heq Ha x)))) ◂ (H (cast Ha x)))
-
-theorem cast_app {A A' : (Type M)} {B : A → (Type M)} {B' : A' → (Type M)}
-                 (f : ∀ x, B x) (a : A) (Ha : A = A') (Hb : (∀ x, B x) = (∀ x, B' x)) :
-      cast Hb f (cast Ha a) == f a
-:= let s1 : cast Hb f == f  := cast_heq Hb f,
-       s2 : cast Ha a == a  := cast_heq Ha a
-   in hcongr s1 s2
-
--- The following theorems can be used as rewriting rules
-
-theorem cast_eq {A : (Type M)} (H : A = A) (a : A) : cast H a = a
-:= to_eq (cast_heq H a)
-
-theorem cast_trans {A B C : (Type M)} (Hab : A = B) (Hbc : B = C) (a : A) : cast Hbc (cast Hab a) = cast (trans Hab Hbc) a
-:= let s1 : cast Hbc (cast Hab a)  == cast Hab a              :=  cast_heq Hbc (cast Hab a),
-       s2 : cast Hab a             == a                       :=  cast_heq Hab a,
-       s3 : cast (trans Hab Hbc) a == a                       :=  cast_heq (trans Hab Hbc) a,
-       s4 : cast Hbc (cast Hab a)  == cast (trans Hab Hbc) a  :=  htrans (htrans s1 s2) (hsymm s3)
-   in to_eq s4
-
-theorem cast_pull {A : (Type M)} {B B' : A → (Type M)}
-                 (f : ∀ x, B x) (a : A) (Hb : (∀ x, B x) = (∀ x, B' x)) (Hba : (B a) = (B' a)) :
-      cast Hb f a = cast Hba (f a)
-:= let s1 : cast Hb f a    == f a    :=  hcongr (cast_heq Hb f) (hrefl a),
-       s2 : cast Hba (f a) == f a    :=  cast_heq Hba (f a)
-   in to_eq (htrans s1 (hsymm s2))
-
--- The following axiom is not very useful, since the resultant
--- equality is actually (@eq TypeM (∀ x, B x) (∀ x, B' x)).
--- This is the case even if A, A', B and B' live in smaller universes (e.g., Type)
--- To support this kind of axiom, it seems we have two options:
---    1) Universe level parameters like Agda
---    2) Axiom schema/template, where we create instances of hpiext for different universes.
---       BTW, this is essentially what Coq does since the levels are implicit in Coq.
--- axiom hpiext {A A' : TypeM} {B : A → TypeM} {B' : A' → TypeM} :
---      A = A' → (∀ x x', x == x' → B x = B' x') → (∀ x, B x) = (∀ x, B' x)
diff --git a/src/builtin/kernel.lean b/src/builtin/kernel.lean
index e33425a79..0d155c5aa 100644
--- a/src/builtin/kernel.lean
+++ b/src/builtin/kernel.lean
@@ -1,3 +1,6 @@
+-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Author: Leonardo de Moura
 import macros
 import tactic
 
@@ -894,11 +897,70 @@ axiom pairext {A : (Type U)} {B : A → (Type U)} {a b : sig x, B x}
               (H1 : proj1 a = proj1 b) (H2 : proj2 a == proj2 b)
               : a = b
 
--- Proof irrelevance, this is true in the set theoretic model we have for Lean.
--- In this model, the interpretation of Bool is the set {{*}, {}}.
--- Thus, if A : Bool is inhabited, then its interpretation must be {*}.
--- So, the interpretation of H1 and H2 must be *.
-axiom hproof_irrel {a b : Bool} (H1 : a) (H2 : b) : H1 == H2
+-- Heterogeneous equality axioms and theorems
+
+-- In the following definitions the type of A and B cannot be (Type U)
+-- because A = B would be @eq (Type U+1) A B, and
+-- the type of eq is (∀T : (Type U), T → T → bool).
+-- So, we define M a universe smaller than U.
+universe M ≥ 1
+definition TypeM := (Type M)
+
+-- We can "type-cast" an A expression into a B expression, if we can prove that A = B
+variable cast {A B : (Type M)} : A = B → A → B
+axiom cast_heq {A B : (Type M)} (H : A = B) (a : A) : cast H a == a
+
+-- Heterogeneous equality satisfies the usual properties: symmetry, transitivity, congruence and function extensionality
+axiom hsymm {A B : (Type U)} {a : A} {b : B} : a == b → b == a
+axiom htrans {A B C : (Type U)} {a : A} {b : B} {c : C} : a == b → b == c → a == c
+axiom hcongr {A A' : (Type U)} {B : A → (Type U)} {B' : A' → (Type U)} {f : ∀ x, B x} {f' : ∀ x, B' x} {a : A} {a' : A'} :
+      f == f' → a == a' → f a == f' a'
+axiom hfunext {A A' : (Type M)} {B : A → (Type U)} {B' : A' → (Type U)} {f : ∀ x, B x} {f' : ∀ x, B' x} :
+      A = A' → (∀ x x', x == x' → f x == f' x') → f == f'
+
+-- Heterogeneous version of the allext theorem
+theorem hallext {A A' : (Type M)} {B : A → Bool} {B' : A' → Bool}
+                (Ha : A = A') (Hb : ∀ x x', x == x' → B x = B' x') : (∀ x, B x) = (∀ x, B' x)
+:= boolext
+     (assume (H : ∀ x : A, B x),
+        take x' : A', (Hb (cast (symm Ha) x') x' (cast_heq (symm Ha) x')) ◂ (H (cast (symm Ha) x')))
+     (assume (H : ∀ x' : A', B' x'),
+        take x : A, (symm (Hb x (cast Ha x) (hsymm (cast_heq Ha x)))) ◂ (H (cast Ha x)))
+
+-- Simpler version of hfunext axiom, we use it to build proofs
+theorem hsfunext {A : (Type M)} {B B' : A → (Type U)} {f : ∀ x, B x} {f' : ∀ x, B' x} :
+      (∀ x, f x == f' x) → f == f'
+:= λ Hb,
+     hfunext (refl A) (λ (x x' : A) (Hx : x == x'),
+                   let s1 : f x   == f' x  := Hb x,
+                       s2 : f' x  == f' x' := hcongr (hrefl f') Hx
+                   in htrans s1 s2)
+
+-- Some theorems that are useful for applying simplifications.
+theorem cast_eq {A : (Type M)} (H : A = A) (a : A) : cast H a = a
+:= to_eq (cast_heq H a)
+
+theorem cast_trans {A B C : (Type M)} (Hab : A = B) (Hbc : B = C) (a : A) : cast Hbc (cast Hab a) = cast (trans Hab Hbc) a
+:= let s1 : cast Hbc (cast Hab a)  == cast Hab a              :=  cast_heq Hbc (cast Hab a),
+       s2 : cast Hab a             == a                       :=  cast_heq Hab a,
+       s3 : cast (trans Hab Hbc) a == a                       :=  cast_heq (trans Hab Hbc) a,
+       s4 : cast Hbc (cast Hab a)  == cast (trans Hab Hbc) a  :=  htrans (htrans s1 s2) (hsymm s3)
+   in to_eq s4
+
+theorem cast_pull {A : (Type M)} {B B' : A → (Type M)}
+                 (f : ∀ x, B x) (a : A) (Hb : (∀ x, B x) = (∀ x, B' x)) (Hba : (B a) = (B' a)) :
+      cast Hb f a = cast Hba (f a)
+:= let s1 : cast Hb f a    == f a    :=  hcongr (cast_heq Hb f) (hrefl a),
+       s2 : cast Hba (f a) == f a    :=  cast_heq Hba (f a)
+   in to_eq (htrans s1 (hsymm s2))
+
+-- Proof irrelevance is true in the set theoretic model we have for Lean.
+axiom proof_irrel {a : Bool} (H1 H2 : a) : H1 = H2
+
+-- A more general version of proof_irrel that can be be derived using proof_irrel, heq axioms and boolext/iff_intro
+theorem hproof_irrel {a b : Bool} (H1 : a) (H2 : b) : H1 == H2
+:= let H1b       : b                     := cast (by simp) H1,
+       H1_eq_H1b : H1 == H1b             := hsymm (cast_heq (by simp) H1),
+       H1b_eq_H2 : H1b == H2             := to_heq (proof_irrel H1b H2)
+   in  htrans H1_eq_H1b H1b_eq_H2
 
-theorem proof_irrel {a : Bool} (H1 H2 : a) : H1 = H2
-:= to_eq (hproof_irrel H1 H2)
\ No newline at end of file
diff --git a/src/builtin/obj/heq.olean b/src/builtin/obj/heq.olean
index fda2c6434..a9360f428 100644
Binary files a/src/builtin/obj/heq.olean and b/src/builtin/obj/heq.olean differ
diff --git a/src/builtin/obj/kernel.olean b/src/builtin/obj/kernel.olean
index b856c463e..2c41e9364 100644
Binary files a/src/builtin/obj/kernel.olean and b/src/builtin/obj/kernel.olean differ
diff --git a/src/kernel/kernel_decls.cpp b/src/kernel/kernel_decls.cpp
index a2445eaca..2234e6d63 100644
--- a/src/kernel/kernel_decls.cpp
+++ b/src/kernel/kernel_decls.cpp
@@ -187,6 +187,18 @@ MK_CONSTANT(non_surjective_fn, name("non_surjective"));
 MK_CONSTANT(ind, name("ind"));
 MK_CONSTANT(infinity, name("infinity"));
 MK_CONSTANT(pairext_fn, name("pairext"));
-MK_CONSTANT(hproof_irrel_fn, name("hproof_irrel"));
+MK_CONSTANT(TypeM, name("TypeM"));
+MK_CONSTANT(cast_fn, name("cast"));
+MK_CONSTANT(cast_heq_fn, name("cast_heq"));
+MK_CONSTANT(hsymm_fn, name("hsymm"));
+MK_CONSTANT(htrans_fn, name("htrans"));
+MK_CONSTANT(hcongr_fn, name("hcongr"));
+MK_CONSTANT(hfunext_fn, name("hfunext"));
+MK_CONSTANT(hallext_fn, name("hallext"));
+MK_CONSTANT(hsfunext_fn, name("hsfunext"));
+MK_CONSTANT(cast_eq_fn, name("cast_eq"));
+MK_CONSTANT(cast_trans_fn, name("cast_trans"));
+MK_CONSTANT(cast_pull_fn, name("cast_pull"));
 MK_CONSTANT(proof_irrel_fn, name("proof_irrel"));
+MK_CONSTANT(hproof_irrel_fn, name("hproof_irrel"));
 }
diff --git a/src/kernel/kernel_decls.h b/src/kernel/kernel_decls.h
index 61a51ec91..b3029d55b 100644
--- a/src/kernel/kernel_decls.h
+++ b/src/kernel/kernel_decls.h
@@ -547,10 +547,46 @@ bool is_infinity(expr const & e);
 expr mk_pairext_fn();
 bool is_pairext_fn(expr const & e);
 inline expr mk_pairext_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_pairext_fn(), e1, e2, e3, e4, e5, e6}); }
-expr mk_hproof_irrel_fn();
-bool is_hproof_irrel_fn(expr const & e);
-inline expr mk_hproof_irrel_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_hproof_irrel_fn(), e1, e2, e3, e4}); }
+expr mk_TypeM();
+bool is_TypeM(expr const & e);
+expr mk_cast_fn();
+bool is_cast_fn(expr const & e);
+inline bool is_cast(expr const & e) { return is_app(e) && is_cast_fn(arg(e, 0)) && num_args(e) == 5; }
+inline expr mk_cast(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_cast_fn(), e1, e2, e3, e4}); }
+expr mk_cast_heq_fn();
+bool is_cast_heq_fn(expr const & e);
+inline expr mk_cast_heq_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_cast_heq_fn(), e1, e2, e3, e4}); }
+expr mk_hsymm_fn();
+bool is_hsymm_fn(expr const & e);
+inline expr mk_hsymm_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_hsymm_fn(), e1, e2, e3, e4, e5}); }
+expr mk_htrans_fn();
+bool is_htrans_fn(expr const & e);
+inline expr mk_htrans_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6, expr const & e7, expr const & e8) { return mk_app({mk_htrans_fn(), e1, e2, e3, e4, e5, e6, e7, e8}); }
+expr mk_hcongr_fn();
+bool is_hcongr_fn(expr const & e);
+inline expr mk_hcongr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6, expr const & e7, expr const & e8, expr const & e9, expr const & e10) { return mk_app({mk_hcongr_fn(), e1, e2, e3, e4, e5, e6, e7, e8, e9, e10}); }
+expr mk_hfunext_fn();
+bool is_hfunext_fn(expr const & e);
+inline expr mk_hfunext_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6, expr const & e7, expr const & e8) { return mk_app({mk_hfunext_fn(), e1, e2, e3, e4, e5, e6, e7, e8}); }
+expr mk_hallext_fn();
+bool is_hallext_fn(expr const & e);
+inline expr mk_hallext_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_hallext_fn(), e1, e2, e3, e4, e5, e6}); }
+expr mk_hsfunext_fn();
+bool is_hsfunext_fn(expr const & e);
+inline expr mk_hsfunext_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_hsfunext_fn(), e1, e2, e3, e4, e5, e6}); }
+expr mk_cast_eq_fn();
+bool is_cast_eq_fn(expr const & e);
+inline expr mk_cast_eq_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_cast_eq_fn(), e1, e2, e3}); }
+expr mk_cast_trans_fn();
+bool is_cast_trans_fn(expr const & e);
+inline expr mk_cast_trans_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_cast_trans_fn(), e1, e2, e3, e4, e5, e6}); }
+expr mk_cast_pull_fn();
+bool is_cast_pull_fn(expr const & e);
+inline expr mk_cast_pull_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6, expr const & e7) { return mk_app({mk_cast_pull_fn(), e1, e2, e3, e4, e5, e6, e7}); }
 expr mk_proof_irrel_fn();
 bool is_proof_irrel_fn(expr const & e);
 inline expr mk_proof_irrel_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_proof_irrel_fn(), e1, e2, e3}); }
+expr mk_hproof_irrel_fn();
+bool is_hproof_irrel_fn(expr const & e);
+inline expr mk_hproof_irrel_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_hproof_irrel_fn(), e1, e2, e3, e4}); }
 }
diff --git a/src/library/heq_decls.cpp b/src/library/heq_decls.cpp
index 70ccf29d6..13acd55d3 100644
--- a/src/library/heq_decls.cpp
+++ b/src/library/heq_decls.cpp
@@ -6,17 +6,4 @@ Released under Apache 2.0 license as described in the file LICENSE.
 #include "kernel/environment.h"
 #include "kernel/decl_macros.h"
 namespace lean {
-MK_CONSTANT(TypeM, name("TypeM"));
-MK_CONSTANT(cast_fn, name("cast"));
-MK_CONSTANT(cast_heq_fn, name("cast_heq"));
-MK_CONSTANT(hsymm_fn, name("hsymm"));
-MK_CONSTANT(htrans_fn, name("htrans"));
-MK_CONSTANT(hcongr_fn, name("hcongr"));
-MK_CONSTANT(hfunext_fn, name("hfunext"));
-MK_CONSTANT(hsfunext_fn, name("hsfunext"));
-MK_CONSTANT(hallext_fn, name("hallext"));
-MK_CONSTANT(cast_app_fn, name("cast_app"));
-MK_CONSTANT(cast_eq_fn, name("cast_eq"));
-MK_CONSTANT(cast_trans_fn, name("cast_trans"));
-MK_CONSTANT(cast_pull_fn, name("cast_pull"));
 }
diff --git a/src/library/heq_decls.h b/src/library/heq_decls.h
index 4e89e43d1..2776d59c2 100644
--- a/src/library/heq_decls.h
+++ b/src/library/heq_decls.h
@@ -5,43 +5,4 @@ Released under Apache 2.0 license as described in the file LICENSE.
 // Automatically generated file, DO NOT EDIT
 #include "kernel/expr.h"
 namespace lean {
-expr mk_TypeM();
-bool is_TypeM(expr const & e);
-expr mk_cast_fn();
-bool is_cast_fn(expr const & e);
-inline bool is_cast(expr const & e) { return is_app(e) && is_cast_fn(arg(e, 0)) && num_args(e) == 5; }
-inline expr mk_cast(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_cast_fn(), e1, e2, e3, e4}); }
-expr mk_cast_heq_fn();
-bool is_cast_heq_fn(expr const & e);
-inline expr mk_cast_heq_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_cast_heq_fn(), e1, e2, e3, e4}); }
-expr mk_hsymm_fn();
-bool is_hsymm_fn(expr const & e);
-inline expr mk_hsymm_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_hsymm_fn(), e1, e2, e3, e4, e5}); }
-expr mk_htrans_fn();
-bool is_htrans_fn(expr const & e);
-inline expr mk_htrans_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6, expr const & e7, expr const & e8) { return mk_app({mk_htrans_fn(), e1, e2, e3, e4, e5, e6, e7, e8}); }
-expr mk_hcongr_fn();
-bool is_hcongr_fn(expr const & e);
-inline expr mk_hcongr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6, expr const & e7, expr const & e8, expr const & e9, expr const & e10) { return mk_app({mk_hcongr_fn(), e1, e2, e3, e4, e5, e6, e7, e8, e9, e10}); }
-expr mk_hfunext_fn();
-bool is_hfunext_fn(expr const & e);
-inline expr mk_hfunext_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6, expr const & e7, expr const & e8) { return mk_app({mk_hfunext_fn(), e1, e2, e3, e4, e5, e6, e7, e8}); }
-expr mk_hsfunext_fn();
-bool is_hsfunext_fn(expr const & e);
-inline expr mk_hsfunext_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_hsfunext_fn(), e1, e2, e3, e4, e5, e6}); }
-expr mk_hallext_fn();
-bool is_hallext_fn(expr const & e);
-inline expr mk_hallext_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_hallext_fn(), e1, e2, e3, e4, e5, e6}); }
-expr mk_cast_app_fn();
-bool is_cast_app_fn(expr const & e);
-inline expr mk_cast_app_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6, expr const & e7, expr const & e8) { return mk_app({mk_cast_app_fn(), e1, e2, e3, e4, e5, e6, e7, e8}); }
-expr mk_cast_eq_fn();
-bool is_cast_eq_fn(expr const & e);
-inline expr mk_cast_eq_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_cast_eq_fn(), e1, e2, e3}); }
-expr mk_cast_trans_fn();
-bool is_cast_trans_fn(expr const & e);
-inline expr mk_cast_trans_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_cast_trans_fn(), e1, e2, e3, e4, e5, e6}); }
-expr mk_cast_pull_fn();
-bool is_cast_pull_fn(expr const & e);
-inline expr mk_cast_pull_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6, expr const & e7) { return mk_app({mk_cast_pull_fn(), e1, e2, e3, e4, e5, e6, e7}); }
 }
diff --git a/tests/lean/univ.lean b/tests/lean/univ.lean
index 3d4074f2f..9906ce40f 100644
--- a/tests/lean/univ.lean
+++ b/tests/lean/univ.lean
@@ -1,20 +1,20 @@
-universe M >= 1
-universe U >= M + 1
-definition TypeM := (Type M)
-universe Z ≥ M+3
+universe M1 >= 1
+universe U >= M1 + 1
+definition TypeM1 := (Type M1)
+universe Z ≥ M1+3
 (*
 local env = get_environment()
-assert(env:get_universe_distance("Z", "M") == 3)
+assert(env:get_universe_distance("Z", "M1") == 3)
 assert(not env:get_universe_distance("Z", "U"))
 *)
 
 (*
 local env = get_environment()
-assert(env:get_universe_distance("Z", "M") == 3)
+assert(env:get_universe_distance("Z", "M1") == 3)
 assert(not env:get_universe_distance("Z", "U"))
 *)
 
-universe Z1 ≥ M + 1073741824.
+universe Z1 ≥ M1 + 1073741824.
 universe Z2 ≥ Z1 + 1073741824.
 
 universe U1
diff --git a/tests/lean/univ.lean.expected.out b/tests/lean/univ.lean.expected.out
index 5927c52d7..1ae285e47 100644
--- a/tests/lean/univ.lean.expected.out
+++ b/tests/lean/univ.lean.expected.out
@@ -1,6 +1,6 @@
   Set: pp::colors
   Set: pp::unicode
-  Defined: TypeM
+  Defined: TypeM1
 univ.lean:18:0: error: universe constraint produces an integer overflow: Z2 >= Z1 + 1073741824
 univ.lean:31:0: error: universe constraint inconsistency: U1 >= U4 + 0
 univ.lean:33:0: error: invalid universe constraint: Z >= U + 0, several modules in Lean assume that U is the maximal universe