diff --git a/src/frontends/lean/notation.cpp b/src/frontends/lean/notation.cpp
index d279046cad..4fdee28792 100644
--- a/src/frontends/lean/notation.cpp
+++ b/src/frontends/lean/notation.cpp
@@ -83,17 +83,21 @@ void init_builtin_notation(environment const & env, io_state & ios) {
     add_coercion(env, mk_nat_to_real_fn());
 
     // implicit arguments for builtin axioms
-    mark_implicit_arguments(env, mk_cast_fn(), 2);
     mark_implicit_arguments(env, mk_mp_fn(), 2);
     mark_implicit_arguments(env, mk_discharge_fn(), 2);
     mark_implicit_arguments(env, mk_refl_fn(), 1);
     mark_implicit_arguments(env, mk_subst_fn(), 4);
     add_alias(env, "Subst", "SubstP");
     mark_implicit_arguments(env, "SubstP", 3);
-    mark_implicit_arguments(env, mk_trans_ext_fn(), 6);
     mark_implicit_arguments(env, mk_eta_fn(), 2);
     mark_implicit_arguments(env, mk_abst_fn(), 4);
     mark_implicit_arguments(env, mk_imp_antisym_fn(), 2);
+    mark_implicit_arguments(env, mk_hsymm_fn(), 4);
+    mark_implicit_arguments(env, mk_htrans_fn(), 6);
+
+    mark_implicit_arguments(env, mk_cast_fn(), 2);
+    mark_implicit_arguments(env, mk_cast_eq_fn(), 2);
+    mark_implicit_arguments(env, mk_cast_app_fn(), 4);
     mark_implicit_arguments(env, mk_dom_inj_fn(), 4);
     mark_implicit_arguments(env, mk_ran_inj_fn(), 4);
 
diff --git a/src/kernel/builtin.cpp b/src/kernel/builtin.cpp
index d9903bf84b..664094de8e 100644
--- a/src/kernel/builtin.cpp
+++ b/src/kernel/builtin.cpp
@@ -196,12 +196,14 @@ MK_CONSTANT(mp_fn,          name("MP"));
 MK_CONSTANT(discharge_fn,   name("Discharge"));
 MK_CONSTANT(case_fn,        name("Case"));
 MK_CONSTANT(refl_fn,        name("Refl"));
-MK_CONSTANT(trans_ext_fn,   name("TransExt"));
 MK_CONSTANT(subst_fn,       name("Subst"));
 MK_CONSTANT(eta_fn,         name("Eta"));
 MK_CONSTANT(imp_antisym_fn, name("ImpAntisym"));
 MK_CONSTANT(abst_fn,        name("Abst"));
 
+MK_CONSTANT(htrans_fn,      name("HTrans"));
+MK_CONSTANT(hsymm_fn,       name("HSymm"));
+
 void import_basic(environment const & env) {
     if (!env->mark_builtin_imported("basic"))
         return;
@@ -269,9 +271,6 @@ void import_basic(environment const & env) {
     // Refl : Pi (A : Type u) (a : A), a = a
     env->add_axiom(refl_fn_name, Pi({{A, TypeU}, {a, A}}, Eq(a, a)));
 
-    // TransExt : Pi (A B C: Type u) (a : A) (b : B) (c : C) (H1 : a = b) (H2 : b = c), a = c
-    env->add_axiom(trans_ext_fn_name, Pi({{A, TypeU}, {B, TypeU}, {C, TypeU}, {a, A}, {b, B}, {c, C}, {H1, Eq(a, b)}, {H2, Eq(b, c)}}, Eq(a, c)));
-
     // Subst : Pi (A : Type u) (a b : A) (P : A -> bool) (H1 : P a) (H2 : a = b), P b
     env->add_axiom(subst_fn_name, Pi({{A, TypeU}, {a, A}, {b, A}, {P, A_pred}, {H1, P(a)}, {H2, Eq(a, b)}}, P(b)));
 
@@ -283,5 +282,11 @@ void import_basic(environment const & env) {
 
     // Abst : Pi (A : Type u) (B : A -> Type u), f g : (Pi x : A, B x), H : (Pi x : A, (f x) = (g x)), f = g
     env->add_axiom(abst_fn_name, Pi({{A, TypeU}, {B, A_arrow_u}, {f, piABx}, {g, piABx}, {H, Pi(x, A, Eq(f(x), g(x)))}}, Eq(f, g)));
+
+    // HSymm : Pi (A B : Type u) (a : A) (b : B) (H1 : a = b), b = a
+    env->add_axiom(hsymm_fn_name, Pi({{A, TypeU}, {B, TypeU}, {a, A}, {b, B}, {H1, Eq(a, b)}}, Eq(b, a)));
+
+    // HTrans : Pi (A B C: Type u) (a : A) (b : B) (c : C) (H1 : a = b) (H2 : b = c), a = c
+    env->add_axiom(htrans_fn_name, Pi({{A, TypeU}, {B, TypeU}, {C, TypeU}, {a, A}, {b, B}, {c, C}, {H1, Eq(a, b)}, {H2, Eq(b, c)}}, Eq(a, c)));
 }
 }
diff --git a/src/kernel/builtin.h b/src/kernel/builtin.h
index 61e283a62a..e58fc65339 100644
--- a/src/kernel/builtin.h
+++ b/src/kernel/builtin.h
@@ -164,13 +164,6 @@ expr mk_subst_fn();
 /** \brief (Axiom) {A : Type u}, {a b : A}, P : A -> Bool, H1 : P a, H2 : a = b |- Subst(A, a, b, P, H1, H2) : P b */
 inline expr Subst(expr const & A, expr const & a, expr const & b, expr const & P, expr const & H1, expr const & H2) { return mk_app({mk_subst_fn(), A, a, b, P, H1, H2}); }
 
-/** \brief Heterogeneous Transitivity axiom */
-expr mk_trans_ext_fn();
-/** \brief (Axiom) {A : Type u}, {B : Type u}, {B : Type u}, {a : A}, {b : B} {c : C}, H1 : a = b, H2 : b = c |- TransExt(A, B, a, b, c, H1, H2) : a = c */
-inline expr TransExt(expr const & A, expr const & B, expr const & C, expr const & a, expr const & b, expr const & c, expr const & H1, expr const & H2) {
-    return mk_app({mk_trans_ext_fn(), A, B, C, a, b, c, H1, H2});
-}
-
 /** \brief Eta conversion axiom */
 expr mk_eta_fn();
 /** \brief (Axiom) {A : Type u}, {B : A -> Type u}, f : (Pi x : A, B x) |- Eta(A, B, f) : ((Fun x : A => f x) = f) */
@@ -186,6 +179,20 @@ expr mk_abst_fn();
 /** \brief (Axiom) {A : Type u} {B : A -> Type u}, f g : {Pi x : A, B x}, H : (Pi x : A, (f x) = (g x)) |- Abst(A, B, f, g, H) : f = g */
 inline expr Abst(expr const & A, expr const & B, expr const & f, expr const & g, expr const & H) { return mk_app({mk_abst_fn(), A, B, f, g, H}); }
 
+/** \brief Heterogeneous symmetry axiom */
+expr mk_hsymm_fn();
+/** \brief (Axiom) {A : Type u}, {B : Type u}, {a : A}, {b : B}, H1 : a = b |- HSymm(A, B, a, b, H1) : b = a */
+inline expr HSymm(expr const & A, expr const & B, expr const & a, expr const & b, expr const & H1) {
+    return mk_app({mk_hsymm_fn(), A, B, a, b, H1});
+}
+
+/** \brief Heterogeneous Transitivity axiom */
+expr mk_htrans_fn();
+/** \brief (Axiom) {A : Type u}, {B : Type u}, {C : Type u}, {a : A}, {b : B} {c : C}, H1 : a = b, H2 : b = c |- TransExt(A, B, a, b, c, H1, H2) : a = c */
+inline expr HTrans(expr const & A, expr const & B, expr const & C, expr const & a, expr const & b, expr const & c, expr const & H1, expr const & H2) {
+    return mk_app({mk_htrans_fn(), A, B, C, a, b, c, H1, H2});
+}
+
 class environment;
 /** \brief Initialize the environment with basic builtin declarations and axioms */
 void import_basic(environment const & env);
diff --git a/src/library/basic_thms.cpp b/src/library/basic_thms.cpp
index 71faea0a56..b9c16997bd 100644
--- a/src/library/basic_thms.cpp
+++ b/src/library/basic_thms.cpp
@@ -253,8 +253,8 @@ void import_basic_thms(environment const & env) {
     // Congr : Pi (A : Type u) (B : A -> Type u) (f g : Pi (x : A) B x) (a b : A) (H1 : f = g) (H2 : a = b), f a = g b
     env->add_theorem(congr_fn_name, Pi({{A, TypeU}, {B, A_arrow_u}, {f, piABx}, {g, piABx}, {a, A}, {b, A}, {H1, Eq(f, g)}, {H2, Eq(a, b)}}, Eq(f(a), g(b))),
                      Fun({{A, TypeU}, {B, A_arrow_u}, {f, piABx}, {g, piABx}, {a, A}, {b, A}, {H1, Eq(f, g)}, {H2, Eq(a, b)}},
-                         TransExt(B(a), B(b), B(b), f(a), f(b), g(b),
-                                  Congr2(A, B, a, b, f, H2), Congr1(A, B, f, g, b, H1))));
+                         HTrans(B(a), B(b), B(b), f(a), f(b), g(b),
+                                Congr2(A, B, a, b, f, H2), Congr1(A, B, f, g, b, H1))));
 
 
     // ForallElim : Pi (A : Type u) (P : A -> bool) (H : (forall A P)) (a : A), P a
diff --git a/src/library/cast/cast.cpp b/src/library/cast/cast.cpp
index 971284fab9..02ee33bfa9 100644
--- a/src/library/cast/cast.cpp
+++ b/src/library/cast/cast.cpp
@@ -13,92 +13,11 @@ Author: Leonardo de Moura
 
 namespace lean {
 // Cast builtin operator
-static name   g_cast_name("Cast");
-static format g_cast_fmt(g_cast_name);
-expr mk_Cast_fn();
-class cast_fn_value : public value {
-    expr m_type;
-public:
-    cast_fn_value() {
-        expr A    = Const("A");
-        expr B    = Const("B");
-        // Cast: Pi (A : Type u) (B : Type u) (H : A = B) (a : A), B
-        m_type = Pi({{A, TypeU}, {B, TypeU}}, Eq(A, B) >> (A >> B));
-    }
-    virtual ~cast_fn_value() {}
-    virtual expr get_type() const { return m_type; }
-    virtual name get_name() const { return g_cast_name; }
-    virtual optional<expr> normalize(unsigned num_as, expr const * as) const {
-        if (num_as > 4 && as[1] == as[2]) {
-            // Cast T T H a == a
-            if (num_as == 5)
-                return some_expr(as[4]);
-            else
-                return some_expr(mk_app(num_as - 4, as + 4));
-        } else if (is_app(as[4]) &&
-                   arg(as[4], 0) == mk_Cast_fn() &&
-                   num_args(as[4]) == 5 &&
-                   as[1] == arg(as[4], 2)) {
-            // Cast T1 T2 H1 (Cast T3 T1 H2 a) == Cast T3 T2 (Trans H1 H2) a
-            expr const & nested = as[4];
-            expr const & T1 = as[1];
-            expr const & T2 = as[2];
-            expr const & T3 = arg(nested, 1);
-            expr const & H1 = as[3];
-            expr const & H2 = arg(nested, 3);
-            expr const & a  = arg(nested, 4);
-            expr c = Cast(T3, T2, Trans(TypeU, T3, T1, T2, H1, H2), a);
-            if (num_as == 5) {
-                return some_expr(c);
-            } else {
-                buffer<expr> new_as;
-                new_as.push_back(c);
-                new_as.append(num_as - 5, as + 5);
-                return some_expr(mk_app(new_as));
-            }
-        } else if (num_as > 5 && is_pi(as[1]) && is_pi(as[2])) {
-            // cast T1 T2 H f a_1 ... a_k
-            // Propagate application over cast.
-            // Remark: we check if T1 is a Pi to prevent non-termination
-            // For example, H can be a bogus hypothesis that shows
-            // that A == A -> A
-
-            // Since T1 and T2 are Pi's, we decompose them
-            expr const & T1  = as[1]; // Pi x : A1, B1
-            expr const & T2  = as[2]; // Pi x : A2, B2
-            expr const & H   = as[3];
-            expr const & f   = as[4];
-            expr const & a_1 = as[5]; // a_1 : A2
-            expr const & A1  = abst_domain(T1);
-            expr const & B1  = abst_body(T1);
-            expr const & A2  = abst_domain(T2);
-            expr const & B2  = abst_body(T2);
-            expr B1f         = mk_lambda(abst_name(T1), A1, B1);
-            expr B2f         = mk_lambda(abst_name(T2), A2, B2);
-            expr A2_eq_A1    = DomInj(A1, A2, B1f, B2f, Symm(TypeU, T1, T2, H));
-            expr a_1p        = Cast(A2, A1, A2_eq_A1, a_1); // a_1p : A1
-            expr fa_1        = f(a_1p);  // fa_1 : (A1 a_1p)
-            // Cast fa_1 back to B2 since the type of cast T1 T2 H f a_1
-            // is in B2 a_1p
-            expr B1_eq_B2_at_a_1p = RanInj(A1, A2, B1f, B2f, H, a_1p);
-            expr fa_1_B2     = Cast(instantiate(B1, 0, a_1p), instantiate(B2, 0, a_1), B1_eq_B2_at_a_1p, fa_1);
-            if (num_as == 6) {
-                return some_expr(fa_1_B2);
-            } else {
-                buffer<expr> new_as;
-                new_as.push_back(fa_1_B2);
-                new_as.append(num_as - 6, as + 6);
-                return some_expr(mk_app(new_as));
-            }
-        } else {
-            return none_expr();
-        }
-    }
-};
-MK_BUILTIN(Cast_fn,     cast_fn_value);
-MK_CONSTANT(cast_fn,    name("cast"));
-MK_CONSTANT(dom_inj_fn, name("DomInj"));
-MK_CONSTANT(ran_inj_fn, name("RanInj"));
+MK_CONSTANT(cast_fn,      name("cast"));
+MK_CONSTANT(cast_eq_fn,   name("CastEq"));
+MK_CONSTANT(cast_app_fn,  name("CastApp"));
+MK_CONSTANT(dom_inj_fn,   name("DomInj"));
+MK_CONSTANT(ran_inj_fn,   name("RanInj"));
 
 void import_cast(environment const & env) {
     if (!env->mark_builtin_imported("cast"))
@@ -111,14 +30,13 @@ void import_cast(environment const & env) {
     expr piABx     = Pi({x, A}, B(x));
     expr piApBpx   = Pi({x, Ap}, Bp(x));
     expr H         = Const("H");
+    expr H1        = Const("H1");
+    expr H2        = Const("H2");
     expr a         = Const("a");
     expr b         = Const("b");
+    expr f         = Const("f");
 
-    env->add_builtin(mk_Cast_fn());
-
-    // Alias for Cast operator. We create the alias to be able to mark
-    // implicit arguments.
-    env->add_definition(cast_fn_name, Pi({{A, TypeU}, {B, TypeU}}, Eq(A, B) >> (A >> B)), mk_Cast_fn());
+    env->add_var(cast_fn_name, Pi({{A, TypeU}, {B, TypeU}}, Eq(A, B) >> (A >> B)));
 
     // DomInj : Pi (A A': Type u) (B : A -> Type u) (B' : A' -> Type u) (H : (Pi x : A, B x) = (Pi x : A', B' x)), A = A'
     env->add_axiom(dom_inj_fn_name, Pi({{A, TypeU}, {Ap, TypeU}, {B, A >> TypeU}, {Bp, Ap >> TypeU}, {H, Eq(piABx, piApBpx)}}, Eq(A, Ap)));
@@ -127,5 +45,14 @@ void import_cast(environment const & env) {
     //                     B a = B' (cast A A' (DomInj A A' B B' H) a)
     env->add_axiom(ran_inj_fn_name, Pi({{A, TypeU}, {Ap, TypeU}, {B, A >> TypeU}, {Bp, Ap >> TypeU}, {H, Eq(piABx, piApBpx)}, {a, A}},
                                        Eq(B(a), Bp(Cast(A, Ap, DomInj(A, Ap, B, Bp, H), a)))));
+
+    // CastEq : Pi (A B : Type u) (H : A == B) (x : A), x == (cast A B H x)
+    env->add_axiom(cast_eq_fn_name, Pi({{A, TypeU}, {B, TypeU}, {H, Eq(A, B)}, {x, A}}, Eq(x, Cast(A, B, H, x))));
+
+    // CastApp : Pi (A A': Type u) (B : A -> Type u) (B' : A' -> Type u) (H1 : (Pi x : A, B x) = (Pi x : A', B' x)) (H2 : A = A')
+    //              (f : Pi x : A, B x) (x : A),  Cast(Pi(x : A, B x), Pi(x : A', B' x), H1, f)(Cast(A, A', H2, x)) ==  f(x)
+    env->add_axiom(cast_app_fn_name, Pi({{A, TypeU},
+                    {Ap, TypeU}, {B, A >> TypeU}, {Bp, Ap >> TypeU}, {H1, Eq(piABx, piApBpx)}, {H2, Eq(A, Ap)}, {f, piABx}, {x, A}},
+            Eq(Cast(piABx, piApBpx, H1, f)(Cast(A, Ap, H2, x)), f(x))));
 }
 }
diff --git a/src/library/cast/cast.h b/src/library/cast/cast.h
index 0a6612d719..2baddf207e 100644
--- a/src/library/cast/cast.h
+++ b/src/library/cast/cast.h
@@ -14,6 +14,21 @@ expr mk_cast_fn();
 inline expr mk_cast(expr const & A, expr const & B, expr const & H, expr const & a) { return mk_app(mk_cast_fn(), A, B, H, a); }
 inline expr Cast(expr const & A, expr const & B, expr const & H, expr const & a) { return mk_cast(A, B, H, a); }
 
+/** \brief Axiom a == (cast A B H a) */
+expr mk_cast_eq_fn();
+inline expr CastEq(expr const & A, expr const & B, expr const & H, expr const & a) { return mk_app({mk_cast_eq_fn(), A, B, H, a}); }
+
+/** \brief Axiom
+    CastApp :
+    Pi (A A': Type u) (B : A -> Type u) (B' : A' -> Type u) (H1 : (Pi x : A, B x) = (Pi x : A', B' x)) (H2 : A = A')
+       (f : Pi x : A, B x) (x : A), Cast(Pi(x : A, B x), Pi(x : A', B' x), H1, f)(Cast(A, A', H2, x)) ==  f(x)
+*/
+expr mk_cast_app_fn();
+inline expr CastApp(expr const & A, expr const & Ap, expr const & B, expr const & Bp, expr const & H1, expr const & H2,
+                    expr const & f, expr const & x) {
+    return mk_app({mk_cast_app_fn(), A, Ap, B, Bp, H1, H2, f, x});
+}
+
 /** \brief Domain Injectivity.
     It has type <tt>Pi (A A': Type u) (B : A -> Type u) (B' : A' -> Type u) (H : (Pi x : A, B x) = (Pi x : A', B' x)), A = A' </tt>
 */
diff --git a/tests/lean/cast3.lean.expected.out b/tests/lean/cast3.lean.expected.out
index 05c72967e7..fdef9bf29b 100644
--- a/tests/lean/cast3.lean.expected.out
+++ b/tests/lean/cast3.lean.expected.out
@@ -5,23 +5,23 @@
   Assumed: B
   Assumed: B'
   Assumed: x
-x
-x == x
+cast (Refl A) x
+x == cast (Refl A) x
   Assumed: b
   Defined: f
   Assumed: H
   Assumed: a'
-b
+cast H (λ x : A, b) a'
   Assumed: H2
   Defined: g
 0
 g (cast H2 f a') : ℕ
-Cast B B' (RanInj H2 (Cast A' A (DomInj (Symm H2)) a')) b
+cast H2 (λ x : A, b) a'
   Assumed: A1
   Assumed: A2
   Assumed: A3
   Assumed: Ha
   Assumed: Hb
   Assumed: a
-Cast A1 A3 (Trans Hb Ha) a
+cast Hb (cast Ha a)
 cast Hb (cast Ha a) : A3
diff --git a/tests/lean/cast4.lean b/tests/lean/cast4.lean
new file mode 100644
index 0000000000..5245a8b446
--- /dev/null
+++ b/tests/lean/cast4.lean
@@ -0,0 +1,29 @@
+SetOption pp::colors false
+
+Definition TypeM := (Type M)
+Definition TypeU := (Type U)
+
+Check fun (A A': TypeM)
+          (B   : A -> TypeM)
+          (B'  : A' -> TypeM)
+          (f   : Pi x : A, B x)
+          (g   : Pi x : A', B' x)
+          (a   : A)
+          (b   : A')
+          (H1  : (Pi x : A, B x) == (Pi x : A', B' x))
+          (H2  : f == g)
+          (H3  : a == b),
+    let
+        S1 : (Pi x : A', B' x) == (Pi x : A, B x) := Symm H1,
+        L2 : A' == A                              := DomInj S1,
+        b' : A                                    := cast L2 b,
+        L3 : b  == b'                             := CastEq L2 b,
+        L4 : a == b'                              := HTrans H3 L3,
+        L5 : f a == f b'                          := Congr2 f L4,
+        g' : (Pi x : A, B x)                      := cast S1 g,
+        L6 : g == g'                              := CastEq S1 g,
+        L7 : f == g'                              := HTrans H2 L6,
+        L8 : f b' == g' b'                        := Congr1 b' L7,
+        L9 : f a == g' b'                         := HTrans L5 L8,
+        L10 : g' b' == g b                        := CastApp S1 L2 g b
+    in HTrans L9 L10
diff --git a/tests/lean/cast4.lean.expected.out b/tests/lean/cast4.lean.expected.out
new file mode 100644
index 0000000000..572dac5c53
--- /dev/null
+++ b/tests/lean/cast4.lean.expected.out
@@ -0,0 +1,30 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Set: pp::colors
+  Defined: TypeM
+  Defined: TypeU
+λ (A A' : TypeM)
+  (B : A → TypeM)
+  (B' : A' → TypeM)
+  (f : Π x : A, B x)
+  (g : Π x : A', B' x)
+  (a : A)
+  (b : A')
+  (H1 : (Π x : A, B x) == (Π x : A', B' x))
+  (H2 : f == g)
+  (H3 : a == b),
+  let S1 : (Π x : A', B' x) == (Π x : A, B x) := Symm H1,
+      L2 : A' == A := DomInj S1,
+      b' : A := cast L2 b,
+      L3 : b == b' := CastEq L2 b,
+      L4 : a == b' := HTrans H3 L3,
+      L5 : f a == f b' := Congr2 f L4,
+      g' : Π x : A, B x := cast S1 g,
+      L6 : g == g' := CastEq S1 g,
+      L7 : f == g' := HTrans H2 L6,
+      L8 : f b' == g' b' := Congr1 b' L7,
+      L9 : f a == g' b' := HTrans L5 L8,
+      L10 : g' b' == g b := CastApp S1 L2 g b
+  in HTrans L9 L10 :
+    Π (A A' : TypeM) (B : A → TypeM) (B' : A' → TypeM) (f : Π x : A, B x) (g : Π x : A', B' x) (a : A) (b : A'),
+      (Π x : A, B x) == (Π x : A', B' x) → f == g → a == b → f a == g b
diff --git a/tests/lean/eq3.lean b/tests/lean/eq3.lean
index a426ea2379..b47afe423f 100644
--- a/tests/lean/eq3.lean
+++ b/tests/lean/eq3.lean
@@ -1,5 +1,3 @@
-
-
 Variable Vector : Nat -> Type
 Variable n  : Nat
 Variable v1 : Vector n
@@ -7,6 +5,6 @@ Variable v2 : Vector (n + 0)
 Variable v3 : Vector (0 + n)
 Axiom H1 : v1 == v2
 Axiom H2 : v2 == v3
-Check TransExt H1 H2
+Check HTrans H1 H2
 SetOption pp::implicit true
-Check TransExt H1 H2
+Check HTrans H1 H2
diff --git a/tests/lean/eq3.lean.expected.out b/tests/lean/eq3.lean.expected.out
index 0efbe8c503..d5542ebabc 100644
--- a/tests/lean/eq3.lean.expected.out
+++ b/tests/lean/eq3.lean.expected.out
@@ -7,6 +7,6 @@
   Assumed: v3
   Assumed: H1
   Assumed: H2
-TransExt H1 H2 : v1 == v3
+HTrans H1 H2 : v1 == v3
   Set: lean::pp::implicit
-@TransExt (Vector n) (Vector (n + 0)) (Vector (0 + n)) v1 v2 v3 H1 H2 : v1 == v3
+@HTrans (Vector n) (Vector (n + 0)) (Vector (0 + n)) v1 v2 v3 H1 H2 : v1 == v3
diff --git a/tests/lean/norm_bug1.lean b/tests/lean/norm_bug1.lean
index 959cf75709..a260788471 100644
--- a/tests/lean/norm_bug1.lean
+++ b/tests/lean/norm_bug1.lean
@@ -2,7 +2,6 @@ SetOption pp::colors false
 
 Definition TypeM := (Type M)
 Definition TypeU := (Type U)
-Variable CastEq {A : TypeU} {A' : TypeU} (H : A == A') (x : A) : x == cast H x
 
 Check fun (A A': TypeM)
           (a   : A)
@@ -26,6 +25,6 @@ Check fun (A A': TypeM)
         L2 : A' == A                := Symm L1,
         b' : A                      := cast L2 b,
         L3 : b  == b'               := CastEq L2 b,
-        L4 : a == b'                := TransExt H3 L3,
+        L4 : a == b'                := HTrans H3 L3,
         L5 : f a == f b'            := Congr2 f L4
     in L5
diff --git a/tests/lean/norm_bug1.lean.expected.out b/tests/lean/norm_bug1.lean.expected.out
index 3f6182352a..1478ae428c 100644
--- a/tests/lean/norm_bug1.lean.expected.out
+++ b/tests/lean/norm_bug1.lean.expected.out
@@ -3,7 +3,6 @@
   Set: pp::colors
   Defined: TypeM
   Defined: TypeU
-  Assumed: CastEq
 λ (A A' : TypeM) (a : A) (b : A') (L2 : A' == A), let b' : A := cast L2 b, L3 : b == b' := CastEq L2 b in L3 :
     Π (A A' : TypeM) (a : A) (b : A') (L2 : A' == A), b == cast L2 b
 λ (A A' : TypeM)
@@ -20,7 +19,7 @@
       L2 : A' == A := Symm L1,
       b' : A := cast L2 b,
       L3 : b == b' := CastEq L2 b,
-      L4 : a == b' := TransExt H3 L3,
+      L4 : a == b' := HTrans H3 L3,
       L5 : f a == f b' := Congr2 f L4
   in L5 :
     Π (A A' : TypeM)
@@ -31,4 +30,4 @@
       (a : A)
       (b : A')
       (H1 : (Π x : A, B x) == (Π x : A', B' x)),
-      f == g → a == b → f a == f (Cast A' A (Symm (DomInj H1)) b)
+      f == g → a == b → f a == f (cast (Symm (DomInj H1)) b)
diff --git a/tests/lean/type_inf_bug1.lean b/tests/lean/type_inf_bug1.lean
index 5256aad8f9..9d13a9034a 100644
--- a/tests/lean/type_inf_bug1.lean
+++ b/tests/lean/type_inf_bug1.lean
@@ -2,14 +2,13 @@ SetOption pp::colors false
 
 Definition TypeM := (Type M)
 Definition TypeU := (Type U)
-Variable MyCastEq {A : TypeU} {A' : TypeU} (H : A == A') (x : A) : x == cast H x
 
 Check fun (A A': TypeM)
           (a   : A)
           (b   : A')
           (L2  : A' == A),
    let b' : A        := cast   L2 b,
-       L3 : b == b'  := MyCastEq L2 b
+       L3 : b == b'  := CastEq L2 b
    in L3
 
 Check fun (A A': TypeM)
@@ -25,13 +24,13 @@ Check fun (A A': TypeM)
     let L1 : A  == A'                             := DomInj H1,
         L2 : A' == A                              := Symm L1,
         b' : A                                    := cast L2 b,
-        L3 : b  == b'                             := MyCastEq L2 b,
-        L4 : a == b'                              := TransExt H3 L3,
+        L3 : b  == b'                             := CastEq L2 b,
+        L4 : a == b'                              := HTrans H3 L3,
         L5 : f a == f b'                          := Congr2 f L4,
         S1 : (Pi x : A', B' x) == (Pi x : A, B x) := Symm H1,
         g' : (Pi x : A, B x)                      := cast S1 g,
-        L6 : g == g'                              := MyCastEq S1 g,
-        L7 : f == g'                              := TransExt H2 L6,
+        L6 : g == g'                              := CastEq S1 g,
+        L7 : f == g'                              := HTrans H2 L6,
         L8 : f b' == g' b'                        := Congr1 b' L7,
-        L9 : f a == g' b'                         := TransExt L5 L8
+        L9 : f a == g' b'                         := HTrans L5 L8
     in L9
diff --git a/tests/lean/type_inf_bug1.lean.expected.out b/tests/lean/type_inf_bug1.lean.expected.out
index 623613bbe5..187415993d 100644
--- a/tests/lean/type_inf_bug1.lean.expected.out
+++ b/tests/lean/type_inf_bug1.lean.expected.out
@@ -3,8 +3,7 @@
   Set: pp::colors
   Defined: TypeM
   Defined: TypeU
-  Assumed: MyCastEq
-λ (A A' : TypeM) (a : A) (b : A') (L2 : A' == A), let b' : A := cast L2 b, L3 : b == b' := MyCastEq L2 b in L3 :
+λ (A A' : TypeM) (a : A) (b : A') (L2 : A' == A), let b' : A := cast L2 b, L3 : b == b' := CastEq L2 b in L3 :
     Π (A A' : TypeM) (a : A) (b : A') (L2 : A' == A), b == cast L2 b
 λ (A A' : TypeM)
   (B : A → TypeM)
@@ -19,15 +18,15 @@
   let L1 : A == A' := DomInj H1,
       L2 : A' == A := Symm L1,
       b' : A := cast L2 b,
-      L3 : b == b' := MyCastEq L2 b,
-      L4 : a == b' := TransExt H3 L3,
+      L3 : b == b' := CastEq L2 b,
+      L4 : a == b' := HTrans H3 L3,
       L5 : f a == f b' := Congr2 f L4,
       S1 : (Π x : A', B' x) == (Π x : A, B x) := Symm H1,
       g' : Π x : A, B x := cast S1 g,
-      L6 : g == g' := MyCastEq S1 g,
-      L7 : f == g' := TransExt H2 L6,
+      L6 : g == g' := CastEq S1 g,
+      L7 : f == g' := HTrans H2 L6,
       L8 : f b' == g' b' := Congr1 b' L7,
-      L9 : f a == g' b' := TransExt L5 L8
+      L9 : f a == g' b' := HTrans L5 L8
   in L9 :
     Π (A A' : TypeM)
       (B : A → TypeM)
@@ -37,4 +36,4 @@
       (a : A)
       (b : A')
       (H1 : (Π x : A, B x) == (Π x : A', B' x)),
-      f == g → a == b → f a == Cast (Π x : A', B' x) (Π x : A, B x) (Symm H1) g (Cast A' A (Symm (DomInj H1)) b)
+      f == g → a == b → f a == cast (Symm H1) g (cast (Symm (DomInj H1)) b)