diff --git a/src/kernel/builtin.cpp b/src/kernel/builtin.cpp
index 8660a3737..2354d8ef6 100644
--- a/src/kernel/builtin.cpp
+++ b/src/kernel/builtin.cpp
@@ -202,7 +202,7 @@ void add_basic_theory(environment & env) {
     env.add_definition(not_fn_name, p1, Fun({x, Bool}, bIf(x, False, True)));
 
     // forall : Pi (A : Type u), (A -> Bool) -> Bool
-    env.add_var(forall_fn_name, q_type);
+    env.add_definition(forall_fn_name, q_type, Fun({{A, TypeU}, {P, A_pred}}, Eq(P, Fun({x, A}, True))));
     env.add_definition(exists_fn_name, q_type, Fun({{A,TypeU}, {P, A_pred}}, Not(Forall(A, Fun({x, A}, Not(P(x)))))));
 
     // refl : Pi (A : Type u) (a : A), a = a
@@ -265,11 +265,14 @@ void add_basic_theory(environment & env) {
                     Fun({{a, Bool}, {H, Eq(a, True)}},
                         EqMP(True, a, Symm(Bool, a, True, H), Truth)));
 
+    // foralle : Pi (A : Type u) (P : A -> bool) (H : (forall A P)) (a : A), P a
+    env.add_theorem(foralle_fn_name, Pi({{A, TypeU}, {P, A_pred}, {H, mk_forall(A, P)}, {a, A}}, P(a)),
+                    Fun({{A, TypeU}, {P, A_pred}, {H, mk_forall(A, P)}, {a, A}},
+                        EqTElim(P(a), Congr1(A, Fun({x, A}, Bool), P, Fun({x, A}, True), a, H))));
+
     // ext : 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(ext_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)));
 
-    // foralle : Pi (A : Type u) (P : A -> bool) (H : (forall A P)) (a : A), P a
-    env.add_axiom(foralle_fn_name, Pi({{A, TypeU}, {P, A_pred}, {H, mk_forall(A, P)}, {a, A}}, P(a)));
     // foralli : Pi (A : Type u) (P : A -> bool) (H : Pi (x : A), P x), (forall A P)
     env.add_axiom(foralli_fn_name, Pi({{A, TypeU}, {P, A_pred}, {H, Pi({x, A}, P(x))}}, Forall(A, P)));
 
diff --git a/src/kernel/builtin.h b/src/kernel/builtin.h
index b7e887c84..8a76719e4 100644
--- a/src/kernel/builtin.h
+++ b/src/kernel/builtin.h
@@ -158,6 +158,16 @@ bool is_truth(expr const & e);
 /** \brief (Theorem) Truth : True */
 #define Truth mk_truth()
 
+expr mk_eqt_elim_fn();
+bool is_eqt_elim(expr const & e);
+// \brief (Theorem) a : Bool, H : a = True |- EqT(a, H) : a
+inline expr EqTElim(expr const & a, expr const & H) { return mk_app(mk_eqt_elim_fn(), a, H); }
+
+expr mk_foralle_fn();
+bool is_foralle_fn(expr const & e);
+// \brief (Theorem) A : Type u, P : A -> Bool, H : (Forall A P), a : A |- Forallelim(A, P, H, a) : P a
+inline expr ForallElim(expr const & A, expr const & P, expr const & H, expr const & a) { return mk_app(mk_foralle_fn(), A, P, H, a); }
+
 expr mk_ext_fn();
 bool is_ext_fn(expr const & e);
 expr mk_foralle_fn();