diff --git a/src/builtin/obj/cast.olean b/src/builtin/obj/cast.olean
index 363cd6d3b..0b2e26624 100644
Binary files a/src/builtin/obj/cast.olean and b/src/builtin/obj/cast.olean differ
diff --git a/tests/lean/bug.lean b/tests/lean/bug.lean
index a525b9897..7b9c486ce 100644
--- a/tests/lean/bug.lean
+++ b/tests/lean/bug.lean
@@ -1 +1 @@
-check fun (A A' : (Type U')) (H : A = A'), symm H
+check fun (A A' : (Type U)) (H : A = A'), symm H
diff --git a/tests/lean/bug.lean.expected.out b/tests/lean/bug.lean.expected.out
index 8d20643d3..3c39a30a2 100644
--- a/tests/lean/bug.lean.expected.out
+++ b/tests/lean/bug.lean.expected.out
@@ -1,8 +1,8 @@
   Set: pp::colors
   Set: pp::unicode
 Failed to solve
-A : (Type U'), A' : (Type U') ⊢ ?M::4 ≺ (Type U')
-    bug.lean:1:37: Type of argument 1 must be convertible to the expected type in the application of
+A : (Type U), A' : (Type U) ⊢ ?M::4 ≺ (Type U)
+    bug.lean:1:36: Type of argument 1 must be convertible to the expected type in the application of
         @eq
     with arguments:
         ?M::0
diff --git a/tests/lean/eq3.lean b/tests/lean/eq3.lean
index 01999f540..a8c4741ae 100644
--- a/tests/lean/eq3.lean
+++ b/tests/lean/eq3.lean
@@ -1,8 +1,9 @@
+import heq
 variable Vector : Nat -> Type
 variable n  : Nat
 variable v1 : Vector n
 variable v2 : Vector (n + 0)
 variable v3 : Vector (0 + n)
-axiom cast {A B : TypeU} : A = B -> A -> B
-axiom H1 : v1 = cast (congr2 Vector (Nat::add_zeror n)) v2
-axiom H2 : v2 = cast (congr2 Vector (Nat::add_comm 0 n)) v3
+axiom H1 : v1 == v2
+axiom H2 : v2 == v3
+check htrans H1 H2
diff --git a/tests/lean/eq3.lean.expected.out b/tests/lean/eq3.lean.expected.out
index 211df19f5..871de95c3 100644
--- a/tests/lean/eq3.lean.expected.out
+++ b/tests/lean/eq3.lean.expected.out
@@ -1,10 +1,11 @@
   Set: pp::colors
   Set: pp::unicode
+  Imported 'heq'
   Assumed: Vector
   Assumed: n
   Assumed: v1
   Assumed: v2
   Assumed: v3
-  Assumed: cast
   Assumed: H1
   Assumed: H2
+htrans H1 H2 : v1 == v3
diff --git a/tests/lean/find.lean.expected.out b/tests/lean/find.lean.expected.out
index 466f89f5c..e403cbf09 100644
--- a/tests/lean/find.lean.expected.out
+++ b/tests/lean/find.lean.expected.out
@@ -1,8 +1,8 @@
   Set: pp::colors
   Set: pp::unicode
   Imported 'find'
-theorem congr1 {A : TypeU'} {B : A → TypeU'} {f g : ∀ x : A, B x} (a : A) (H : f = g) : f a = g a
-theorem congr2 {A B : TypeU'} {a b : A} (f : A → B) (H : a = b) : f a = f b
-theorem congr {A B : TypeU'} {f g : A → B} {a b : A} (H1 : f = g) (H2 : a = b) : f a = g b
+theorem congr1 {A : TypeU} {B : A → TypeU} {f g : ∀ x : A, B x} (a : A) (H : f = g) : f a = g a
+theorem congr2 {A B : TypeU} {a b : A} (f : A → B) (H : a = b) : f a = f b
+theorem congr {A B : TypeU} {f g : A → B} {a b : A} (H1 : f = g) (H2 : a = b) : f a = g b
 find.lean:3:0: error: executing external script (/home/leo/projects/lean/build/debug/shell/find.lua:24), no object name in the environment matches the regular expression 'foo'
 find.lean:4:0: error: executing external script (/home/leo/projects/lean/build/debug/shell/find.lua:18), unfinished capture
diff --git a/tests/lean/tst11.lean.expected.out b/tests/lean/tst11.lean.expected.out
index 9830b2040..02af3b075 100644
--- a/tests/lean/tst11.lean.expected.out
+++ b/tests/lean/tst11.lean.expected.out
@@ -6,7 +6,7 @@
 ⊤
   Assumed: a
 a ⊕ a ⊕ a
-@subst : ∀ (A : TypeU') (a b : A) (P : A → Bool), P a → a = b → P b
+@subst : ∀ (A : TypeU) (a b : A) (P : A → Bool), P a → a = b → P b
   Proved: EM2
 EM2 : ∀ a : Bool, a ∨ ¬ a
 EM2 a : a ∨ ¬ a
diff --git a/tests/lean/tst4.lean.expected.out b/tests/lean/tst4.lean.expected.out
index 71a1b8a37..6201629bc 100644
--- a/tests/lean/tst4.lean.expected.out
+++ b/tests/lean/tst4.lean.expected.out
@@ -10,7 +10,7 @@
   Assumed: EqNice
 @EqNice N n1 n2
 @f N n1 n2 : N
-@congr : ∀ (A B : TypeU') (f g : A → B) (a b : A), @eq (A → B) f g → @eq A a b → @eq B (f a) (g b)
+@congr : ∀ (A B : TypeU) (f g : A → B) (a b : A), @eq (A → B) f g → @eq A a b → @eq B (f a) (g b)
 @f N n1 n2
   Assumed: a
   Assumed: b