diff --git a/src/kernel/builtin.cpp b/src/kernel/builtin.cpp
index 1d01e6d05c..f9b306724e 100644
--- a/src/kernel/builtin.cpp
+++ b/src/kernel/builtin.cpp
@@ -160,8 +160,9 @@ MK_CONSTANT(homo_eq_fn, name("eq"));
 // Axioms
 MK_CONSTANT(mp_fn,          name("MP"));
 MK_CONSTANT(discharge_fn,   name("Discharge"));
-MK_CONSTANT(refl_fn,        name("Refl"));
 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"));
@@ -175,11 +176,13 @@ void import_basic(environment & env) {
     expr f         = Const("f");
     expr a         = Const("a");
     expr b         = Const("b");
+    expr c         = Const("c");
     expr x         = Const("x");
     expr y         = Const("y");
     expr A         = Const("A");
     expr A_pred    = A >> Bool;
     expr B         = Const("B");
+    expr C         = Const("C");
     expr q_type    = Pi({A, TypeU}, A_pred >> Bool);
     expr piABx     = Pi({x, A}, B(x));
     expr A_arrow_u = A >> TypeU;
@@ -222,11 +225,14 @@ void import_basic(environment & env) {
     // Discharge : Pi (a b : Bool) (H : a -> b), a => b
     env.add_axiom(discharge_fn_name, Pi({{a, Bool}, {b, Bool}, {H, a >> b}}, Implies(a, b)));
 
+    // Case : Pi (P : Bool -> Bool) (H1 : P True) (H2 : P False) (a : Bool), P a
+    env.add_axiom(case_fn_name, Pi({{P, Bool >> Bool}, {H1, P(True)}, {H2, P(False)}, {a, Bool}}, P(a)));
+
     // Refl : Pi (A : Type u) (a : A), a = a
     env.add_axiom(refl_fn_name, Pi({{A, TypeU}, {a, A}}, Eq(a, a)));
 
-    // Case : Pi (P : Bool -> Bool) (H1 : P True) (H2 : P False) (a : Bool), P a
-    env.add_axiom(case_fn_name, Pi({{P, Bool >> Bool}, {H1, P(True)}, {H2, P(False)}, {a, Bool}}, P(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)));
diff --git a/src/kernel/builtin.h b/src/kernel/builtin.h
index c85a55eac5..7d2ed1e4db 100644
--- a/src/kernel/builtin.h
+++ b/src/kernel/builtin.h
@@ -123,21 +123,28 @@ expr mk_discharge_fn();
 /** \brief (Axiom) {a : Bool}, {b : Bool}, H : a -> b |- Discharge(a, b, H) : a => b */
 inline expr Discharge(expr const & a, expr const & b, expr const & H) { return mk_app(mk_discharge_fn(), a, b, H); }
 
-/** \brief Reflexivity axiom */
-expr mk_refl_fn();
-/** \brief (Axiom) {A : Type u}, a : A |- Refl(A, a) : a = a */
-inline expr Refl(expr const & A, expr const & a) { return mk_app(mk_refl_fn(), A, a); }
-
 /** \brief Case analysis axiom */
 expr mk_case_fn();
 /** \brief (Axiom) P : Bool -> Bool, H1 : P True, H2 : P False, a : Bool |- Case(P, H1, H2, a) : P a */
 inline expr Case(expr const & P, expr const & H1, expr const & H2, expr const & a) { return mk_app(mk_case_fn(), P, H1, H2, a); }
 
+/** \brief Reflexivity axiom */
+expr mk_refl_fn();
+/** \brief (Axiom) {A : Type u}, a : A |- Refl(A, a) : a = a */
+inline expr Refl(expr const & A, expr const & a) { return mk_app(mk_refl_fn(), A, a); }
+
 /** \brief Substitution axiom */
 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) */
diff --git a/src/library/basic_thms.cpp b/src/library/basic_thms.cpp
index d1c437d5e2..0a6f03bf66 100644
--- a/src/library/basic_thms.cpp
+++ b/src/library/basic_thms.cpp
@@ -32,7 +32,6 @@ MK_CONSTANT(disj2_fn,           name("Disj2"));
 MK_CONSTANT(disj_cases_fn,      name("DisjCases"));
 MK_CONSTANT(symm_fn,            name("Symm"));
 MK_CONSTANT(trans_fn,           name("Trans"));
-MK_CONSTANT(trans_ext_fn,       name("TransExt"));
 MK_CONSTANT(congr1_fn,          name("Congr1"));
 MK_CONSTANT(congr2_fn,          name("Congr2"));
 MK_CONSTANT(congr_fn,           name("Congr"));
@@ -207,11 +206,6 @@ void import_basic_thms(environment & env) {
                     Fun({{A, TypeU}, {a, A}, {b, A}, {c, A}, {H1, Eq(a, b)}, {H2, Eq(b, c)}},
                         Subst(A, b, c, Fun({x, A}, Eq(a, x)), H1, H2)));
 
-    // TransExt: Pi (A: Type u) (B : Type u) (a : A) (b c : B) (H1 : a = b) (H2 : b = c), a = c
-    env.add_theorem(trans_ext_fn_name, Pi({{A, TypeU}, {B, TypeU}, {a, A}, {b, B}, {c, B}, {H1, Eq(a, b)}, {H2, Eq(b, c)}}, Eq(a, c)),
-                    Fun({{A, TypeU}, {B, TypeU}, {a, A}, {b, B}, {c, B}, {H1, Eq(a, b)}, {H2, Eq(b, c)}},
-                        Subst(B, b, c, Fun({x, B}, Eq(a, x)), H1, H2)));
-
     // EqTElim : Pi (a : Bool) (H : a = True), a
     env.add_theorem(eqt_elim_fn_name, Pi({{a, Bool}, {H, Eq(a, True)}}, a),
                     Fun({{a, Bool}, {H, Eq(a, True)}},
@@ -258,7 +252,7 @@ void import_basic_thms(environment & 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), f(a), f(b), g(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))));
 
 
diff --git a/src/library/basic_thms.h b/src/library/basic_thms.h
index c3c3295483..ce2884180c 100644
--- a/src/library/basic_thms.h
+++ b/src/library/basic_thms.h
@@ -92,10 +92,6 @@ expr mk_trans_fn();
 /** \brief (Theorem) {A : Type u}, {a b c : A}, H1 : a = b, H2 : b = c |- Trans(A, a, b, c, H1, H2) : a = c */
 inline expr Trans(expr const & A, expr const & a, expr const & b, expr const & c, expr const & H1, expr const & H2) { return mk_app({mk_trans_fn(), A, a, b, c, H1, H2}); }
 
-expr mk_trans_ext_fn();
-/** \brief (Theorem) {A : Type u}, {B : Type u}, {a : A}, {b c : B}, 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 & a, expr const & b, expr const & c, expr const & H1, expr const & H2) { return mk_app({mk_trans_ext_fn(), A, B, a, b, c, H1, H2}); }
-
 expr mk_eqt_elim_fn();
 /** \brief (Theorem) {a : Bool}, H : a = True |- EqTElim(a, H) : a */
 inline expr EqTElim(expr const & a, expr const & H) { return mk_app(mk_eqt_elim_fn(), a, H); }