diff --git a/examples/lean/dep_if.lean b/examples/lean/dep_if.lean
index 71f0c9975..e89113c32 100644
--- a/examples/lean/dep_if.lean
+++ b/examples/lean/dep_if.lean
@@ -10,14 +10,14 @@ import tactic
 -- We define the "dependent" if-then-else using Hilbert's choice operator ε.
 -- Note that ε is only applicable to non-empty types. Thus, we first
 -- prove the following auxiliary theorem.
-theorem nonempty_resolve {A : TypeU} {c : Bool} (t : c → A) (e : ¬ c → A) : nonempty A
+theorem inhabited_resolve {A : TypeU} {c : Bool} (t : c → A) (e : ¬ c → A) : inhabited A
 := or_elim (em c)
-      (λ Hc,  nonempty_range (nonempty_intro t) Hc)
-      (λ Hnc, nonempty_range (nonempty_intro e) Hnc)
+      (λ Hc,  inhabited_range (inhabited_intro t) Hc)
+      (λ Hnc, inhabited_range (inhabited_intro e) Hnc)
 
 -- The actual definition
 definition dep_if {A : TypeU} (c : Bool) (t : c → A) (e : ¬ c → A) : A
-:= ε (nonempty_resolve t e) (λ r, (∀ Hc : c, r = t Hc) ∧ (∀ Hnc : ¬ c, r = e Hnc))
+:= ε (inhabited_resolve t e) (λ r, (∀ Hc : c, r = t Hc) ∧ (∀ Hnc : ¬ c, r = e Hnc))
 
 theorem then_simp (A : TypeU) (c : Bool) (r : A) (t : c → A) (e : ¬ c → A) (H : c)
                   : (∀ Hc : c, r = t Hc) ∧ (∀ Hnc : ¬ c, r = e Hnc) ↔ r = t H
@@ -35,9 +35,9 @@ theorem then_simp (A : TypeU) (c : Bool) (r : A) (t : c → A) (e : ¬ c → A)
 theorem dep_if_elim_then  {A : TypeU} (c : Bool) (t : c → A) (e : ¬ c → A) (H : c)   : dep_if c t e = t H
 := let s1 : (λ r, (∀ Hc : c, r = t Hc) ∧ (∀ Hnc : ¬ c, r = e Hnc)) = (λ r, r = t H)
           := funext (λ r, then_simp A c r t e H)
-   in calc dep_if c t e  =  ε (nonempty_resolve t e) (λ r, (∀ Hc : c, r = t Hc) ∧ (∀ Hnc : ¬ c, r = e Hnc)) : refl (dep_if c t e)
-                  ...    =  ε (nonempty_resolve t e) (λ r, r = t H) : { s1 }
-                  ...    =  t H                                     : eps_singleton (nonempty_resolve t e) (t H)
+   in calc dep_if c t e  =  ε (inhabited_resolve t e) (λ r, (∀ Hc : c, r = t Hc) ∧ (∀ Hnc : ¬ c, r = e Hnc)) : refl (dep_if c t e)
+                  ...    =  ε (inhabited_resolve t e) (λ r, r = t H) : { s1 }
+                  ...    =  t H                                     : eps_singleton (inhabited_resolve t e) (t H)
 
 theorem dep_if_true {A : TypeU} (t : true → A) (e : ¬ true → A) : dep_if true t e = t trivial
 := dep_if_elim_then true t e trivial
@@ -58,12 +58,12 @@ theorem else_simp (A : TypeU) (c : Bool) (r : A) (t : c → A) (e : ¬ c → A)
 theorem dep_if_elim_else {A : TypeU} (c : Bool) (t : c → A) (e : ¬ c → A) (H : ¬ c) : dep_if c t e = e H
 := let s1 : (λ r, (∀ Hc : c, r = t Hc) ∧ (∀ Hnc : ¬ c, r = e Hnc)) = (λ r, r = e H)
           := funext (λ r, else_simp A c r t e H)
-   in calc dep_if c t e = ε (nonempty_resolve t e) (λ r, (∀ Hc : c, r = t Hc) ∧ (∀ Hnc : ¬ c, r = e Hnc)) : refl (dep_if c t e)
-                    ... = ε (nonempty_resolve t e) (λ r, r = e H) : { s1 }
-                    ... = e H                                     : eps_singleton (nonempty_resolve t e) (e H)
+   in calc dep_if c t e = ε (inhabited_resolve t e) (λ r, (∀ Hc : c, r = t Hc) ∧ (∀ Hnc : ¬ c, r = e Hnc)) : refl (dep_if c t e)
+                    ... = ε (inhabited_resolve t e) (λ r, r = e H) : { s1 }
+                    ... = e H                                     : eps_singleton (inhabited_resolve t e) (e H)
 
-theorem dep_if_false {A : TypeU} (t : false → A) (e : ¬ false → A) : dep_if false t e = e trivial
-:= dep_if_elim_else false t e trivial
+theorem dep_if_false {A : TypeU} (t : false → A) (e : ¬ false → A) : dep_if false t e = e not_false_trivial
+:= dep_if_elim_else false t e not_false_trivial
 
 import cast
 
diff --git a/examples/lean/ex4.lean b/examples/lean/ex4.lean
index e470b12d3..adc9f50e3 100644
--- a/examples/lean/ex4.lean
+++ b/examples/lean/ex4.lean
@@ -1,8 +1,5 @@
 import Int
 import tactic
+set_option simplifier::unfold true -- allow the simplifier to unfold definitions
 definition a : Nat := 10
--- Trivial indicates a "proof by evaluation"
-theorem T1 : a > 0 := trivial
-theorem T2 : a - 5 > 3 := trivial
--- The next one is commented because it fails
--- theorem T3 : a > 11 := trivial
+theorem T1 : a > 0 := (by simp)
diff --git a/src/builtin/Nat.lean b/src/builtin/Nat.lean
index 92c94d039..11beb542d 100644
--- a/src/builtin/Nat.lean
+++ b/src/builtin/Nat.lean
@@ -44,7 +44,7 @@ theorem induction_on {P : Nat → Bool} (a : Nat) (H1 : P 0) (H2 : ∀ (n : Nat)
 
 theorem pred_nz {a : Nat} : a ≠ 0 → ∃ b, b + 1 = a
 := induction_on a
-    (λ H : 0 ≠ 0, false_elim (∃ b, b + 1 = 0) H)
+    (λ H : 0 ≠ 0, false_elim (∃ b, b + 1 = 0) (a_neq_a_elim H))
     (λ (n : Nat) (iH : n ≠ 0 → ∃ b, b + 1 = n) (H : n + 1 ≠ 0),
        or_elim (em (n = 0))
            (λ Heq0 : n = 0, exists_intro 0 (calc 0 + 1 = n + 1 : { symm Heq0 }))
@@ -60,7 +60,7 @@ theorem discriminate {B : Bool} {a : Nat} (H1: a = 0 → B) (H2 : ∀ n, a = n +
 
 theorem add_zerol (a : Nat) : 0 + a = a
 := induction_on a
-    (have 0 + 0 = 0 : trivial)
+    (have 0 + 0 = 0 : add_zeror 0)
     (λ (n : Nat) (iH : 0 + n = n),
         calc  0 + (n + 1)  =  (0 + n) + 1   :  add_succr 0 n
                     ...    =  n + 1         :  { iH })
@@ -95,11 +95,11 @@ theorem add_assoc (a b c : Nat) : (a + b) + c = a + (b + c)
 
 theorem mul_zerol (a : Nat) : 0 * a = 0
 := induction_on a
-    (have 0 * 0 = 0 : trivial)
+    (have 0 * 0 = 0 : mul_zeror 0)
     (λ (n : Nat) (iH : 0 * n = 0),
         calc  0 * (n + 1)  =  (0 * n) + 0 : mul_succr 0 n
                       ...  =  0 + 0       : { iH }
-                      ...  =  0           : trivial)
+                      ...  =  0           : add_zerol 0)
 
 theorem mul_succl (a b : Nat) : (a + 1) * b = a * b + b
 := induction_on b
@@ -118,14 +118,14 @@ theorem mul_succl (a b : Nat) : (a + 1) * b = a * b + b
 
 theorem mul_onel (a : Nat) : 1 * a = a
 := induction_on a
-    (have 1 * 0 = 0 : trivial)
+    (have 1 * 0 = 0 : mul_zeror 1)
     (λ (n : Nat) (iH : 1 * n = n),
         calc  1 * (n + 1)  =  1 * n + 1 :  mul_succr 1 n
                       ...  =  n + 1     : { iH })
 
 theorem mul_oner (a : Nat) : a * 1 = a
 := induction_on a
-    (have 0 * 1 = 0 : trivial)
+    (have 0 * 1 = 0 : mul_zeror 1)
     (λ (n : Nat) (iH : n * 1 = n),
         calc  (n + 1) * 1  =  n * 1 + 1 : mul_succl n 1
                       ...  =  n + 1     : { iH })
@@ -142,7 +142,7 @@ theorem mul_comm (a b : Nat) : a * b = b * a
 theorem distributer (a b c : Nat) : a * (b + c) = a * b + a * c
 := induction_on a
     (calc 0 * (b + c)   = 0              : mul_zerol (b + c)
-                  ...   = 0 + 0          : trivial
+                  ...   = 0 + 0          : add_zeror 0
                   ...   = 0 * b + 0      : { symm (mul_zerol b) }
                   ...   = 0 * b + 0 * c  : { symm (mul_zerol c) })
     (λ (n : Nat) (iH : n * (b + c) = n * b + n * c),
@@ -223,7 +223,6 @@ theorem le_refl (a : Nat) : a ≤ a := le_intro (add_zeror a)
 
 theorem le_zero (a : Nat) : 0 ≤ a := le_intro (add_zerol a)
 
-
 theorem le_trans {a b c : Nat} (H1 : a ≤ b) (H2 : b ≤ c) : a ≤ c
 := obtain (w1 : Nat) (Hw1 : a + w1 = b), from (le_elim H1),
    obtain (w2 : Nat) (Hw2 : b + w2 = c), from (le_elim H2),
@@ -353,8 +352,9 @@ set_opaque add true
 set_opaque mul true
 set_opaque le true
 set_opaque id true
-set_opaque ge true
-set_opaque lt true
-set_opaque gt true
-set_opaque id true
+-- We should only mark constants as opaque after we proved the theorems/properties we need.
+-- set_opaque ge true
+-- set_opaque lt true
+-- set_opaque gt true
+-- set_opaque id true
 end
\ No newline at end of file
diff --git a/src/builtin/cast.lean b/src/builtin/cast.lean
index d09e26189..2fc7ea68e 100644
--- a/src/builtin/cast.lean
+++ b/src/builtin/cast.lean
@@ -1,29 +1 @@
 import heq
-
-variable cast {A B : TypeM} : A = B → A → B
-
-axiom cast_heq {A B : TypeM} (H : A = B) (a : A) : cast H a == a
-
-theorem cast_app {A A' : TypeM} {B : A → TypeM} {B' : A' → TypeM} (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 : TypeM} (H : A = A) (a : A) : cast H a = a
-:= to_eq (cast_heq H a)
-
-theorem cast_trans {A B C : TypeM} (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 : TypeM} {B B' : A → TypeM} (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))
diff --git a/src/builtin/heq.lean b/src/builtin/heq.lean
index 8bc994b37..6321f7e77 100644
--- a/src/builtin/heq.lean
+++ b/src/builtin/heq.lean
@@ -1,40 +1,28 @@
--- Heterogenous equality
-variable heq {A B : TypeU} : A → B → Bool
-infixl 50 == : heq
-
-axiom heq_eq {A : TypeU} (a b : A) : a == b ↔ a = b
-
-theorem to_eq {A : TypeU} {a b : A} (H : a == b) : a = b
-:= (heq_eq a b) ◂ H
-
-theorem to_heq {A : TypeU} {a b : A} (H : a = b) : a == b
-:= (symm (heq_eq a b)) ◂ H
-
-theorem hrefl {A : TypeU} (a : A) : a == a
-:= to_heq (refl a)
-
-theorem heqt_elim {a : Bool} (H : a == true) : a
-:= eqt_elim (to_eq H)
-
-axiom hsymm {A B : TypeU} {a : A} {b : B} : a == b → b == a
-
-axiom htrans {A B C : TypeU} {a : A} {b : B} {c : C} : a == b → b == c → a == c
-
-axiom hcongr {A A' : TypeU} {B : A → TypeU} {B' : A' → TypeU} {f : ∀ x, B x} {f' : ∀ x, B' x} {a : A} {a' : A'} :
-      f == f' → a == a' → f a == f' a'
+-- 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)
 
--- In the following definitions the type of A and A' cannot be TypeU
--- because A = A' would be @eq (Type U+1) A A', and
--- the type of eq is (∀T : (Type U), T → T → bool).
--- So, we define M a universe smaller than U.
+variable cast {A B : (Type M)} : A = B → A → B
 
-axiom hfunext {A A' : TypeM} {B : A → TypeU} {B' : A' → TypeU} {f : ∀ x, B x} {f' : ∀ x, B' x} :
+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 : TypeM} {B B' : A → TypeU} {f : ∀ x, B x} {f' : ∀ x, B' x} :
+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'),
@@ -42,8 +30,39 @@ theorem hsfunext {A : TypeM} {B B' : A → TypeU} {f : ∀ x, B x} {f' : ∀ x,
                        s2 : f' x  == f' x' := hcongr (hrefl f') Hx
                    in htrans s1 s2)
 
-axiom hallext {A A' : TypeM} {B : A → Bool} {B' : A' → Bool} :
-      A = A' → (∀ x x', x == x' → B x = B' x') → (∀ x, B x) = (∀ x, B' x)
+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)).
diff --git a/src/builtin/kernel.lean b/src/builtin/kernel.lean
index 080da2172..45aa54ac3 100644
--- a/src/builtin/kernel.lean
+++ b/src/builtin/kernel.lean
@@ -2,12 +2,43 @@ import macros
 import tactic
 
 universe U ≥ 1
-definition TypeU  := (Type U)
+definition TypeU := (Type U)
+
+-- create default rewrite rule set
+(* mk_rewrite_rule_set() *)
 
 variable Bool : Type
--- The following builtin declarations can be removed as soon as Lean supports inductive datatypes and match expressions
-builtin true : Bool
-builtin false : Bool
+-- Heterogeneous equality
+variable heq {A B : (Type U)} (a : A) (b : B) : Bool
+infixl 50 == : heq
+
+-- Reflexivity for heterogeneous equality
+axiom hrefl {A : (Type U)} (a : A) : a == a
+
+-- Homogeneous equality
+definition eq {A : (Type U)} (a b : A) := a == b
+infix 50 = : eq
+
+theorem refl {A : (Type U)} (a : A) : a = a
+:= hrefl a
+
+theorem heq_eq {A : (Type U)} (a b : A) : (a == b) = (a = b)
+:= refl (a == b)
+
+definition true : Bool
+:= (λ x : Bool, x) = (λ x : Bool, x)
+
+theorem trivial : true
+:= refl (λ x : Bool, x)
+
+set_opaque true true
+
+definition false : Bool
+:= ∀ x : Bool, x
+
+set_opaque false true
+alias ⊤ : true
+alias ⊥ : false
 
 definition not (a : Bool) := a → false
 notation 40 ¬ _ : not
@@ -24,16 +55,25 @@ infixr 35 ∧  : and
 
 definition implies (a b : Bool) := a → b
 
-builtin eq {A : (Type U)} (a b : A) : Bool
-infix 50 = : eq
-
-definition neq {A : TypeU} (a b : A) := ¬ (a = b)
+definition neq {A : (Type U)} (a b : A) := ¬ (a = b)
 infix 50 ≠ : neq
 
+theorem a_neq_a_elim {A : (Type U)} {a : A} (H : a ≠ a) : false
+:= H (refl a)
+
 definition iff (a b : Bool) := a = b
 infixr 25 <-> : iff
 infixr 25 ↔   : iff
 
+theorem em (a : Bool) : a ∨ ¬ a
+:= assume Hna : ¬ a, Hna
+
+theorem not_intro {a : Bool} (H : a → false) : ¬ a
+:= H
+
+theorem absurd {a : Bool} (H1 : a) (H2 : ¬ a) : false
+:= H2 H1
+
 -- The Lean parser has special treatment for the constant exists.
 -- It allows us to write
 --      exists x y : A, P x y   and    ∃ x y : A, P x y
@@ -42,103 +82,14 @@ infixr 25 ↔   : iff
 -- That is, it treats the exists as an extra binder such as fun and forall.
 -- It also provides an alias (Exists) that should be used when we
 -- want to treat exists as a constant.
-definition Exists (A : TypeU) (P : A → Bool) := ¬ (∀ x, ¬ (P x))
-
-definition nonempty (A : TypeU) := ∃ x : A, true
-
--- If we have an element of type A, then A is nonempty
-theorem nonempty_intro {A : TypeU} (a : A) : nonempty A
-:= assume H : (∀ x, ¬ true), (H a)
-
-theorem em (a : Bool) : a ∨ ¬ a
-:= assume Hna : ¬ a, Hna
+definition Exists (A : (Type U)) (P : A → Bool)
+:= ¬ (∀ x, ¬ (P x))
 
 axiom case (P : Bool → Bool) (H1 : P true) (H2 : P false) (a : Bool) : P a
 
-axiom refl {A : TypeU} (a : A) : a = a
-
-axiom subst {A : TypeU} {a b : A} {P : A → Bool} (H1 : P a) (H2 : a = b) : P b
-
--- Function extensionality
-axiom funext {A : TypeU} {B : A → TypeU} {f g : ∀ x : A, B x} (H : ∀ x : A, f x = g x) : f = g
-
--- Forall extensionality
-axiom allext {A : TypeU} {B C : A → Bool} (H : ∀ x : A, B x = C x) : (∀ x : A, B x) = (∀ x : A, C x)
-
--- Epsilon (Hilbert's operator)
-variable eps {A : TypeU} (H : nonempty A) (P : A → Bool) : A
-alias ε : eps
-axiom eps_ax {A : TypeU} (H : nonempty A) {P : A → Bool} (a : A) : P a → P (ε H P)
-
--- Proof irrelevance
-axiom proof_irrel {a : Bool} (H1 H2 : a) : H1 = H2
-
--- Alias for subst where we can provide P explicitly, but keep A,a,b implicit
-theorem substp {A : TypeU} {a b : A} (P : A → Bool) (H1 : P a) (H2 : a = b) : P b
-:= subst H1 H2
-
-theorem eps_th {A : TypeU} {P : A → Bool} (a : A) : P a → P (ε (nonempty_intro a) P)
-:= assume H : P a, @eps_ax A (nonempty_intro a) P a H
-
-theorem eps_singleton {A : TypeU} (H : nonempty A) (a : A) : ε H (λ x, x = a) = a
-:= let P         :=  λ x, x = a,
-       Ha : P a  :=  refl a
-   in eps_ax H a Ha
-
--- A function space (∀ x : A, B x) is nonempty if forall a : A, we have nonempty (B a)
-theorem nonempty_fun {A : TypeU} {B : A → TypeU} (Hn : ∀ a, nonempty (B a)) : nonempty (∀ x, B x)
-:= nonempty_intro (λ x, ε (Hn x) (λ y, true))
-
--- if-then-else expression
-definition ite {A : TypeU} (c : Bool) (a b : A) : A
-:= ε (nonempty_intro a) (λ r, (c → r = a) ∧ (¬ c → r = b))
-notation 45 if _ then _ else _ : ite
-
--- We will mark 'not' as opaque later
-theorem not_intro {a : Bool} (H : a → false) : ¬ a
-:= H
-
-theorem eta {A : TypeU} {B : A → TypeU} (f : ∀ x : A, B x) : (λ x : A, f x) = f
-:= funext (λ x : A, refl (f x))
-
--- create default rewrite rule set
-(* mk_rewrite_rule_set() *)
-
-theorem trivial : true
-:= refl true
-
-theorem absurd {a : Bool} (H1 : a) (H2 : ¬ a) : false
-:= H2 H1
-
-theorem eqmp {a b : Bool} (H1 : a = b) (H2 : a) : b
-:= subst H2 H1
-
-infixl 100 <| : eqmp
-infixl 100 ◂  : eqmp
-
-theorem boolcomplete (a : Bool) : a = true ∨ a = false
-:= case (λ x, x = true ∨ x = false) trivial trivial a
-
 theorem false_elim (a : Bool) (H : false) : a
 := case (λ x, x) trivial H a
 
-theorem imp_trans {a b c : Bool} (H1 : a → b) (H2 : b → c) : a → c
-:= assume Ha, H2 (H1 Ha)
-
-theorem imp_eq_trans {a b c : Bool} (H1 : a → b) (H2 : b = c) : a → c
-:= assume Ha, H2 ◂ (H1 Ha)
-
-theorem eq_imp_trans {a b c : Bool} (H1 : a = b) (H2 : b → c) : a → c
-:= assume Ha, H2 (H1 ◂ Ha)
-
-theorem not_not_eq (a : Bool) : ¬ ¬ a ↔ a
-:= case (λ x, ¬ ¬ x ↔ x) trivial trivial a
-
-add_rewrite not_not_eq
-
-theorem not_not_elim {a : Bool} (H : ¬ ¬ a) : a
-:= (not_not_eq a) ◂ H
-
 theorem mt {a b : Bool} (H1 : a → b) (H2 : ¬ b) : ¬ a
 := assume Ha : a, absurd (H1 Ha) H2
 
@@ -148,29 +99,6 @@ theorem contrapos {a b : Bool} (H : a → b) : ¬ b → ¬ a
 theorem absurd_elim {a : Bool} (b : Bool) (H1 : a) (H2 : ¬ a) : b
 := false_elim b (absurd H1 H2)
 
-theorem not_imp_eliml {a b : Bool} (Hnab : ¬ (a → b)) : a
-:= not_not_elim
-      (have ¬ ¬ a :
-          assume Hna : ¬ a, absurd (assume Ha : a, absurd_elim b Ha Hna)
-                                   Hnab)
-
-theorem not_imp_elimr {a b : Bool} (H : ¬ (a → b)) : ¬ b
-:= assume Hb : b, absurd (assume Ha : a, Hb)
-                         H
-
-theorem resolve1 {a b : Bool} (H1 : a ∨ b) (H2 : ¬ a) : b
-:= H1 H2
-
--- Recall that and is defined as ¬ (a → ¬ b)
-theorem and_intro {a b : Bool} (H1 : a) (H2 : b) : a ∧ b
-:= assume H : a → ¬ b, absurd H2 (H H1)
-
-theorem and_eliml {a b : Bool} (H : a ∧ b) : a
-:= not_imp_eliml H
-
-theorem and_elimr {a b : Bool} (H : a ∧ b) : b
-:= not_not_elim (not_imp_elimr H)
-
 -- Recall that or is defined as ¬ a → b
 theorem or_introl {a : Bool} (H : a) (b : Bool) : a ∨ b
 := assume H1 : ¬ a, absurd_elim b H H1
@@ -178,23 +106,82 @@ theorem or_introl {a : Bool} (H : a) (b : Bool) : a ∨ b
 theorem or_intror {b : Bool} (a : Bool) (H : b) : a ∨ b
 := assume H1 : ¬ a, H
 
-theorem or_elim {a b c : Bool} (H1 : a ∨ b) (H2 : a → c) (H3 : b → c) : c
-:= not_not_elim
-     (assume H : ¬ c,
-        absurd (have c : H3 (have b : resolve1 H1 (have ¬ a : (mt (assume Ha : a, H2 Ha) H))))
-               H)
+theorem boolcomplete (a : Bool) : a = true ∨ a = false
+:= case (λ x, x = true ∨ x = false)
+        (or_introl (refl true) (true = false))
+        (or_intror (false = true) (refl false))
+        a
 
-theorem refute {a : Bool} (H : ¬ a → false) : a
-:= or_elim (em a) (λ H1 : a, H1) (λ H1 : ¬ a, false_elim a (H H1))
+theorem boolcomplete_swapped (a : Bool) : a = false ∨ a = true
+:= case (λ x, x = false ∨ x = true)
+        (or_intror (true = false) (refl true))
+        (or_introl (refl false) (false = true))
+        a
 
-theorem symm {A : TypeU} {a b : A} (H : a = b) : b = a
+theorem resolve1 {a b : Bool} (H1 : a ∨ b) (H2 : ¬ a) : b
+:= H1 H2
+
+axiom subst {A : (Type U)} {a b : A} {P : A → Bool} (H1 : P a) (H2 : a = b) : P b
+
+-- Alias for subst where we provide P explicitly, but keep A,a,b implicit
+theorem substp {A : (Type U)} {a b : A} (P : A → Bool) (H1 : P a) (H2 : a = b) : P b
+:= subst H1 H2
+
+theorem symm {A : (Type U)} {a b : A} (H : a = b) : b = a
 := subst (refl a) H
 
+theorem trans {A : (Type U)} {a b c : A} (H1 : a = b) (H2 : b = c) : a = c
+:= subst H1 H2
+
+theorem congr1 {A B : (Type U)} {f g : A → B} (a : A) (H : f = g) : f a = g a
+:= substp (fun h : A → B, f a = h a) (refl (f a)) H
+
+theorem congr2 {A B : (Type U)} {a b : A} (f : A → B) (H : a = b) : f a = f b
+:= substp (fun x : A, f a = f x) (refl (f a)) H
+
+theorem congr {A B : (Type U)} {f g : A → B} {a b : A} (H1 : f = g) (H2 : a = b) : f a = g b
+:= subst (congr2 f H2) (congr1 b H1)
+
+theorem true_ne_false : ¬ true = false
+:= assume H : true = false,
+     subst trivial H
+
+theorem absurd_not_true (H : ¬ true) : false
+:= absurd trivial H
+
+theorem not_false_trivial : ¬ false
+:= assume H : false, H
+
+-- "equality modus pones"
+theorem eqmp {a b : Bool} (H1 : a = b) (H2 : a) : b
+:= subst H2 H1
+
+infixl 100 <| : eqmp
+infixl 100 ◂  : eqmp
+
 theorem eqmpr {a b : Bool} (H1 : a = b) (H2 : b) : a
 := (symm H1) ◂ H2
 
-theorem trans {A : TypeU} {a b c : A} (H1 : a = b) (H2 : b = c) : a = c
-:= subst H1 H2
+theorem imp_trans {a b c : Bool} (H1 : a → b) (H2 : b → c) : a → c
+:= assume Ha, H2 (H1 Ha)
+
+theorem imp_eq_trans {a b c : Bool} (H1 : a → b) (H2 : b = c) : a → c
+:= assume Ha, H2 ◂ (H1 Ha)
+
+theorem eq_imp_trans {a b c : Bool} (H1 : a = b) (H2 : b → c) : a → c
+:= assume Ha, H2 (H1 ◂ Ha)
+
+theorem to_eq {A : TypeU} {a b : A} (H : a == b) : a = b
+:= (heq_eq a b) ◂ H
+
+theorem to_heq {A : TypeU} {a b : A} (H : a = b) : a == b
+:= (symm (heq_eq a b)) ◂ H
+
+theorem iff_eliml {a b : Bool} (H : a ↔ b) : a → b
+:= (λ Ha : a, eqmp H Ha)
+
+theorem iff_elimr {a b : Bool} (H : a ↔ b) : b → a
+:= (λ Hb : b, eqmpr H Hb)
 
 theorem ne_symm {A : TypeU} {a b : A} (H : a ≠ b) : b ≠ a
 := assume H1 : b = a, H (symm H1)
@@ -211,41 +198,72 @@ theorem eqt_elim {a : Bool} (H : a = true) : a
 theorem eqf_elim {a : Bool} (H : a = false) : ¬ a
 := not_intro (λ Ha : a, H ◂ Ha)
 
-theorem congr1 {A B : TypeU} {f g : A → B} (a : A) (H : f = g) : f a = g a
-:= substp (fun h : A → B, f a = h a) (refl (f a)) H
+theorem heqt_elim {a : Bool} (H : a == true) : a
+:= eqt_elim (to_eq H)
 
-theorem congr2 {A B : TypeU} {a b : A} (f : A → B) (H : a = b) : f a = f b
-:= substp (fun x : A, f a = f x) (refl (f a)) H
+theorem not_true : (¬ true) = false
+:= let aux : ¬ (¬ true) = true
+           := assume H : (¬ true) = true,
+                absurd_not_true (subst trivial (symm H))
+   in resolve1 (boolcomplete (¬ true)) aux
 
-theorem congr {A B : TypeU} {f g : A → B} {a b : A} (H1 : f = g) (H2 : a = b) : f a = g b
-:= subst (congr2 f H2) (congr1 b H1)
+theorem not_false : (¬ false) = true
+:= let aux : ¬ (¬ false) = false
+           := assume H : (¬ false) = false,
+                subst not_false_trivial H
+   in resolve1 (boolcomplete_swapped (¬ false)) aux
 
--- Recall that exists is defined as ¬ ∀ x : A, ¬ P x
-theorem exists_elim {A : TypeU} {P : A → Bool} {B : Bool} (H1 : Exists A P) (H2 : ∀ (a : A) (H : P a), B) : B
-:= refute (λ R : ¬ B,
-             absurd (take a : A, mt (assume H : P a, H2 a H) R)
-                    H1)
+add_rewrite not_true not_false
 
-theorem exists_intro {A : TypeU} {P : A → Bool} (a : A) (H : P a) : Exists A P
-:= assume H1 : (∀ x : A, ¬ P x),
-      absurd H (H1 a)
+theorem not_not_eq (a : Bool) : (¬ ¬ a) = a
+:= case (λ x, (¬ ¬ x) = x)
+        (calc (¬ ¬ true)  = (¬ false) : { not_true }
+                    ...   = true      : not_false)
+        (calc (¬ ¬ false) = (¬ true)  : { not_false }
+                    ...   = false     : not_true)
+        a
 
-theorem nonempty_elim {A : TypeU} (H1 : nonempty A) {B : Bool} (H2 : A → B) : B
-:= obtain (w : A) (Hw : true), from H1,
-     H2 w
+add_rewrite not_not_eq
 
-theorem nonempty_ex_intro {A : TypeU} {P : A → Bool} (H : ∃ x, P x) : nonempty A
-:= obtain (w : A) (Hw : P w), from H,
-      exists_intro w trivial
+theorem not_neq {A : TypeU} (a b : A) : ¬ (a ≠ b) ↔ a = b
+:= not_not_eq (a = b)
 
-theorem exists_to_eps {A : TypeU} {P : A → Bool} (H : ∃ x, P x) : P (ε (nonempty_ex_intro H) P)
-:= obtain (w : A) (Hw : P w), from H,
-      eps_ax (nonempty_ex_intro H) w Hw
+add_rewrite not_neq
 
-theorem axiom_of_choice {A : TypeU} {B : A → TypeU} {R : ∀ x : A, B x → Bool} (H : ∀ x, ∃ y, R x y) : ∃ f, ∀ x, R x (f x)
-:= exists_intro
-      (λ x, ε (nonempty_ex_intro (H x)) (λ y, R x y)) -- witness for f
-      (λ x, exists_to_eps (H x))                      -- proof that witness satisfies ∀ x, R x (f x)
+theorem not_neq_elim {A : TypeU} {a b : A} (H : ¬ (a ≠ b)) : a = b
+:= (not_neq a b) ◂ H
+
+theorem not_not_elim {a : Bool} (H : ¬ ¬ a) : a
+:= (not_not_eq a) ◂ H
+
+theorem not_imp_eliml {a b : Bool} (Hnab : ¬ (a → b)) : a
+:= not_not_elim
+      (have ¬ ¬ a :
+          assume Hna : ¬ a, absurd (assume Ha : a, absurd_elim b Ha Hna)
+                                   Hnab)
+
+theorem not_imp_elimr {a b : Bool} (H : ¬ (a → b)) : ¬ b
+:= assume Hb : b, absurd (assume Ha : a, Hb)
+                         H
+
+-- Recall that and is defined as ¬ (a → ¬ b)
+theorem and_intro {a b : Bool} (H1 : a) (H2 : b) : a ∧ b
+:= assume H : a → ¬ b, absurd H2 (H H1)
+
+theorem and_eliml {a b : Bool} (H : a ∧ b) : a
+:= not_imp_eliml H
+
+theorem and_elimr {a b : Bool} (H : a ∧ b) : b
+:= not_not_elim (not_imp_elimr H)
+
+theorem or_elim {a b c : Bool} (H1 : a ∨ b) (H2 : a → c) (H3 : b → c) : c
+:= not_not_elim
+     (assume H : ¬ c,
+        absurd (have c : H3 (have b : resolve1 H1 (have ¬ a : (mt (assume Ha : a, H2 Ha) H))))
+               H)
+
+theorem refute {a : Bool} (H : ¬ a → false) : a
+:= or_elim (em a) (λ H1 : a, H1) (λ H1 : ¬ a, false_elim a (H H1))
 
 theorem boolext {a b : Bool} (Hab : a → b) (Hba : b → a) : a = b
 := or_elim (boolcomplete a)
@@ -256,23 +274,10 @@ theorem boolext {a b : Bool} (Hab : a → b) (Hba : b → a) : a = b
            (λ Hbt : b = true,  false_elim (a = b) (subst (Hba (eqt_elim Hbt)) Haf))
            (λ Hbf : b = false, trans Haf (symm Hbf)))
 
+-- Another name for boolext
 theorem iff_intro {a b : Bool} (Hab : a → b) (Hba : b → a) : a ↔ b
 := boolext Hab Hba
 
-theorem iff_eliml {a b : Bool} (H : a ↔ b) : a → b
-:= (λ Ha : a, eqmp H Ha)
-
-theorem iff_elimr {a b : Bool} (H : a ↔ b) : b → a
-:= (λ Hb : b, eqmpr H Hb)
-
-theorem skolem_th {A : TypeU} {B : A → TypeU} {P : ∀ x : A, B x → Bool} :
-        (∀ x, ∃ y, P x y) ↔ ∃ f, (∀ x, P x (f x))
-:= iff_intro
-      (λ H : (∀ x, ∃ y, P x y), axiom_of_choice H)
-      (λ H : (∃ f, (∀ x, P x (f x))),
-             take x, obtain (fw : ∀ x, B x) (Hw : ∀ x, P x (fw x)), from H,
-                  exists_intro (fw x) (Hw x))
-
 theorem eqt_intro {a : Bool} (H : a) : a = true
 := boolext (assume H1 : a,    trivial)
            (assume H2 : true, H)
@@ -281,19 +286,26 @@ theorem eqf_intro {a : Bool} (H : ¬ a) : a = false
 := boolext (assume H1 : a,     absurd H1 H)
            (assume H2 : false, false_elim a H2)
 
-theorem neq_elim {A : TypeU} {a b : A} (H : a ≠ b) : a = b ↔ false
-:= eqf_intro H
+theorem a_neq_a {A : (Type U)} (a : A) : (a ≠ a) ↔ false
+:= boolext (assume H, a_neq_a_elim H)
+           (assume H, false_elim (a ≠ a) H)
 
-theorem eq_id {A : TypeU} (a : A) : (a = a) ↔ true
+theorem eq_id {A : (Type U)} (a : A) : (a = a) ↔ true
 := eqt_intro (refl a)
 
 theorem iff_id (a : Bool) : (a ↔ a) ↔ true
 := eqt_intro (refl a)
 
-add_rewrite eq_id iff_id
+theorem neq_elim {A : (Type U)} {a b : A} (H : a ≠ b) : a = b ↔ false
+:= eqf_intro H
+
+theorem neq_to_not_eq {A : (Type U)} {a b : A} : a ≠ b ↔ ¬ a = b
+:= refl (a ≠ b)
+
+add_rewrite eq_id iff_id neq_to_not_eq
 
 -- Remark: ordered rewriting + assoc + comm + left_comm sorts a term lexicographically
-theorem left_comm {A : TypeU} {R : A -> A -> A} (comm : ∀ x y, R x y = R y x) (assoc : ∀ x y z, R (R x y) z = R x (R y z)) :
+theorem left_comm {A : (Type U)} {R : A -> A -> A} (comm : ∀ x y, R x y = R y x) (assoc : ∀ x y z, R (R x y) z = R x (R y z)) :
         ∀ x y z, R x (R y z) = R y (R x z)
 := take x y z, calc R x (R y z) = R (R x y) z : symm (assoc x y z)
                          ...    = R (R y x) z : { comm x y }
@@ -325,7 +337,8 @@ theorem or_falser (a : Bool) : false ∨ a ↔ a
 := trans (or_comm false a) (or_falsel a)
 
 theorem or_truel (a : Bool) : true ∨ a ↔ true
-:= eqt_intro (case (λ x : Bool, true ∨ x) trivial trivial a)
+:= boolext (assume H : true ∨ a, trivial)
+           (assume H : true, or_introl trivial a)
 
 theorem or_truer (a : Bool) : a ∨ true ↔ true
 := trans (or_comm a true) (or_truel a)
@@ -338,6 +351,9 @@ theorem or_left_comm (a b c : Bool) : a ∨ (b ∨ c) ↔ b ∨ (a ∨ c)
 
 add_rewrite or_comm or_assoc or_id or_falsel or_falser or_truel or_truer or_tauto or_left_comm
 
+theorem resolve2 {a b : Bool} (H1 : a ∨ b) (H2 : ¬ b) : a
+:= resolve1 ((or_comm a b) ◂ H1) H2
+
 theorem and_comm (a b : Bool) : a ∧ b ↔ b ∧ a
 := boolext (assume H, and_intro (and_elimr H) (and_eliml H))
            (assume H, and_intro (and_elimr H) (and_eliml H))
@@ -374,16 +390,19 @@ theorem and_left_comm (a b c : Bool) : a ∧ (b ∧ c) ↔ b ∧ (a ∧ c)
 add_rewrite and_comm and_assoc and_id and_falsel and_falser and_truel and_truer and_absurd and_left_comm
 
 theorem imp_truer (a : Bool) : (a → true) ↔ true
-:= case (λ x, (x → true) ↔ true) trivial trivial a
+:= boolext (assume H, trivial)
+           (assume H Ha, trivial)
 
 theorem imp_truel (a : Bool) : (true → a) ↔ a
-:= case (λ x, (true → x) ↔ x) trivial trivial a
+:= boolext (assume H : true → a, H trivial)
+           (assume Ha H, Ha)
 
 theorem imp_falser (a : Bool) : (a → false) ↔ ¬ a
 := refl _
 
 theorem imp_falsel (a : Bool) : (false → a) ↔ true
-:= case (λ x, (false → x) ↔ true) trivial trivial a
+:= boolext (assume H, trivial)
+           (assume H Hf, false_elim a Hf)
 
 theorem imp_id (a : Bool) : (a → a) ↔ true
 := eqt_intro (λ H : a, H)
@@ -391,7 +410,7 @@ theorem imp_id (a : Bool) : (a → a) ↔ true
 add_rewrite imp_truer imp_truel imp_falser imp_falsel imp_id
 
 theorem imp_or (a b : Bool) : (a → b) ↔ ¬ a ∨ b
-:= iff_intro
+:= boolext
      (assume H : a → b,
         (or_elim (em a)
            (λ Ha  : a,   or_intror (¬ a) (H Ha))
@@ -400,83 +419,18 @@ theorem imp_or (a b : Bool) : (a → b) ↔ ¬ a ∨ b
         assume Ha : a,
           resolve1 H ((symm (not_not_eq a)) ◂ Ha))
 
-theorem not_true : ¬ true ↔ false
-:= trivial
-
-theorem not_false : ¬ false ↔ true
-:= trivial
-
-theorem not_neq {A : TypeU} (a b : A) : ¬ (a ≠ b) ↔ a = b
-:= not_not_eq (a = b)
-
-add_rewrite not_true not_false not_neq
-
-theorem not_neq_elim {A : TypeU} {a b : A} (H : ¬ (a ≠ b)) : a = b
-:= (not_neq a b) ◂ H
-
-theorem not_and (a b : Bool) : ¬ (a ∧ b) ↔ ¬ a ∨ ¬ b
-:= case (λ x, ¬ (x ∧ b) ↔ ¬ x ∨ ¬ b)
-        (case (λ y, ¬ (true ∧ y) ↔ ¬ true ∨ ¬ y)   trivial trivial b)
-        (case (λ y, ¬ (false ∧ y) ↔ ¬ false ∨ ¬ y) trivial trivial b)
-        a
-
-theorem not_and_elim {a b : Bool} (H : ¬ (a ∧ b)) : ¬ a ∨ ¬ b
-:= (not_and a b) ◂ H
-
-theorem not_or (a b : Bool) : ¬ (a ∨ b) ↔ ¬ a ∧ ¬ b
-:= case (λ x, ¬ (x ∨ b) ↔ ¬ x ∧ ¬ b)
-        (case (λ y, ¬ (true ∨ y) ↔ ¬ true ∧ ¬ y)   trivial trivial b)
-        (case (λ y, ¬ (false ∨ y) ↔ ¬ false ∧ ¬ y) trivial trivial b)
-        a
-
-theorem not_or_elim {a b : Bool} (H : ¬ (a ∨ b)) : ¬ a ∧ ¬ b
-:= (not_or a b) ◂ H
-
-theorem not_iff (a b : Bool) : ¬ (a ↔ b) ↔ (¬ a ↔ b)
-:= case (λ x, ¬ (x ↔ b) ↔ ((¬ x) ↔ b))
-        (case (λ y, ¬ (true ↔ y) ↔ ((¬ true) ↔ y)) trivial trivial b)
-        (case (λ y, ¬ (false ↔ y) ↔ ((¬ false) ↔ y)) trivial trivial b)
-        a
-
-theorem not_iff_elim {a b : Bool} (H : ¬ (a ↔ b)) : (¬ a) ↔ b
-:= (not_iff a b) ◂ H
-
-theorem not_implies (a b : Bool) : ¬ (a → b) ↔ a ∧ ¬ b
-:= case (λ x, ¬ (x → b) ↔ x ∧ ¬ b)
-        (case (λ y, ¬ (true → y) ↔ true ∧ ¬ y) trivial trivial b)
-        (case (λ y, ¬ (false → y) ↔ false ∧ ¬ y) trivial trivial b)
-        a
-
-theorem not_implies_elim {a b : Bool} (H : ¬ (a → b)) : a ∧ ¬ b
-:= (not_implies a b) ◂ H
-
 theorem not_congr {a b : Bool} (H : a ↔ b) : ¬ a ↔ ¬ b
 := congr2 not H
 
-theorem exists_rem {A : TypeU} (H : nonempty A) (p : Bool) : (∃ x : A, p) ↔ p
-:= iff_intro
-    (assume Hl : (∃ x : A, p),
-       obtain (w : A) (Hw : p), from Hl,
-         Hw)
-    (assume Hr : p,
-       nonempty_elim H (λ w, exists_intro w Hr))
+-- Recall that exists is defined as ¬ ∀ x : A, ¬ P x
+theorem exists_elim {A : TypeU} {P : A → Bool} {B : Bool} (H1 : Exists A P) (H2 : ∀ (a : A) (H : P a), B) : B
+:= refute (λ R : ¬ B,
+             absurd (take a : A, mt (assume H : P a, H2 a H) R)
+                    H1)
 
-theorem forall_rem {A : TypeU} (H : nonempty A) (p : Bool) : (∀ x : A, p) ↔ p
-:= iff_intro
-    (assume Hl : (∀ x : A, p),
-       nonempty_elim H (λ w, Hl w))
-    (assume Hr : p,
-       take x, Hr)
-
-theorem eq_exists_intro {A : (Type U)} {P Q : A → Bool} (H : ∀ x : A, P x ↔ Q x) : (∃ x : A, P x) ↔ (∃ x : A, Q x)
-:= congr2 (Exists A) (funext H)
-
-theorem not_forall (A : (Type U)) (P : A → Bool) : ¬ (∀ x : A, P x) ↔ (∃ x : A, ¬ P x)
-:= calc (¬ ∀ x : A, P x) = ¬ ∀ x : A, ¬ ¬ P x : not_congr (allext (λ x : A, symm (not_not_eq (P x))))
-              ...        = ∃ x : A, ¬ P x     : refl (∃ x : A, ¬ P x)
-
-theorem not_forall_elim {A : (Type U)} {P : A → Bool} (H : ¬ (∀ x : A, P x)) : ∃ x : A, ¬ P x
-:= (not_forall A P) ◂ H
+theorem exists_intro {A : TypeU} {P : A → Bool} (a : A) (H : P a) : Exists A P
+:= assume H1 : (∀ x : A, ¬ P x),
+      absurd H (H1 a)
 
 theorem not_exists (A : (Type U)) (P : A → Bool) : ¬ (∃ x : A, P x) ↔ (∀ x : A, ¬ P x)
 := calc (¬ ∃ x : A, P x) = ¬ ¬ ∀ x : A, ¬ P x : refl (¬ ∃ x : A, P x)
@@ -504,6 +458,46 @@ theorem exists_unfold {A : TypeU} (P : A → Bool) (a : A) : (∃ x : A, P x) 
 := boolext (assume H : (∃ x : A, P x),                 exists_unfold1 a H)
            (assume H : (P a ∨ (∃ x : A, x ≠ a ∧ P x)), exists_unfold2 a H)
 
+definition inhabited (A : (Type U))
+:= ∃ x : A, true
+
+-- If we have an element of type A, then A is inhabited
+theorem inhabited_intro {A : TypeU} (a : A) : inhabited A
+:= assume H : (∀ x, ¬ true), absurd_not_true (H a)
+
+theorem inhabited_elim {A : TypeU} (H1 : inhabited A) {B : Bool} (H2 : A → B) : B
+:= obtain (w : A) (Hw : true), from H1,
+     H2 w
+
+theorem inhabited_ex_intro {A : TypeU} {P : A → Bool} (H : ∃ x, P x) : inhabited A
+:= obtain (w : A) (Hw : P w), from H,
+      exists_intro w trivial
+
+-- If a function space is non-empty, then for every 'a' in the domain, the range (B a) is not empty
+theorem inhabited_range {A : TypeU} {B : A → TypeU} (H : inhabited (∀ x, B x)) (a : A) : inhabited (B a)
+:= refute (λ N : ¬ inhabited (B a),
+     let s1 : ¬ ∃ x : B a, true       := N,
+         s2 : ∀ x : B a, false        := take x : B a, absurd_not_true (not_exists_elim s1 x),
+         s3 : ∃ y : (∀ x, B x), true := H
+     in obtain (w : (∀ x, B x)) (Hw : true), from s3,
+           let s4 : B a := w a
+           in s2 s4)
+
+theorem exists_rem {A : TypeU} (H : inhabited A) (p : Bool) : (∃ x : A, p) ↔ p
+:= iff_intro
+    (assume Hl : (∃ x : A, p),
+       obtain (w : A) (Hw : p), from Hl,
+         Hw)
+    (assume Hr : p,
+       inhabited_elim H (λ w, exists_intro w Hr))
+
+theorem forall_rem {A : TypeU} (H : inhabited A) (p : Bool) : (∀ x : A, p) ↔ p
+:= iff_intro
+    (assume Hl : (∀ x : A, p),
+       inhabited_elim H (λ w, Hl w))
+    (assume Hr : p,
+       take x, Hr)
+
 -- Congruence theorems for contextual simplification
 
 -- Simplify a → b, by first simplifying a to c using the fact that ¬ b is true, and then
@@ -588,6 +582,87 @@ theorem and_congrl {a b c d : Bool} (H_bd : ∀ (H_a : a), b = d) (H_ac : ∀ (H
 theorem and_congr {a b c d : Bool} (H_ac : a = c) (H_bd : ∀ (H_c : c), b = d) : a ∧ b ↔ c ∧ d
 := and_congrr (λ H, H_ac) H_bd
 
+theorem not_and (a b : Bool) : ¬ (a ∧ b) ↔ ¬ a ∨ ¬ b
+:= boolext (assume H, or_elim (em a)
+               (assume Ha, or_elim (em b)
+                     (assume Hb, absurd_elim (¬ a ∨ ¬ b) (and_intro Ha Hb) H)
+                     (assume Hnb, or_intror (¬ a) Hnb))
+               (assume Hna, or_introl Hna (¬ b)))
+           (assume (H : ¬ a ∨ ¬ b) (N : a ∧ b),
+               or_elim H
+                 (assume Hna, absurd (and_eliml N) Hna)
+                 (assume Hnb, absurd (and_elimr N) Hnb))
+
+theorem not_and_elim {a b : Bool} (H : ¬ (a ∧ b)) : ¬ a ∨ ¬ b
+:= (not_and a b) ◂ H
+
+theorem not_or (a b : Bool) : ¬ (a ∨ b) ↔ ¬ a ∧ ¬ b
+:= boolext (assume H, or_elim (em a)
+               (assume Ha, absurd_elim (¬ a ∧ ¬ b) (or_introl Ha b) H)
+               (assume Hna, or_elim (em b)
+                   (assume Hb, absurd_elim (¬ a ∧ ¬ b) (or_intror a Hb) H)
+                   (assume Hnb, and_intro Hna Hnb)))
+           (assume (H : ¬ a ∧ ¬ b) (N : a ∨ b),
+               or_elim N
+                 (assume Ha, absurd Ha (and_eliml H))
+                 (assume Hb, absurd Hb (and_elimr H)))
+
+theorem not_or_elim {a b : Bool} (H : ¬ (a ∨ b)) : ¬ a ∧ ¬ b
+:= (not_or a b) ◂ H
+
+theorem not_implies (a b : Bool) : ¬ (a → b) ↔ a ∧ ¬ b
+:= calc (¬ (a → b)) = ¬ (¬ a ∨ b)  : { imp_or a b }
+                 ... = ¬ ¬ a ∧ ¬ b  : not_or (¬ a) b
+                 ... = a ∧ ¬ b      : by simp
+
+theorem not_implies_elim {a b : Bool} (H : ¬ (a → b)) : a ∧ ¬ b
+:= (not_implies a b) ◂ H
+
+theorem a_eq_not_a (a : Bool) : (a = ¬ a) ↔ false
+:= boolext (λ H, or_elim (em a)
+                 (λ Ha, absurd Ha (subst Ha H))
+                 (λ Hna, absurd (subst Hna (symm H)) Hna))
+           (λ H, false_elim (a = ¬ a) H)
+
+theorem a_iff_not_a (a : Bool) : (a ↔ ¬ a) ↔ false
+:= a_eq_not_a a
+
+theorem true_eq_false : (true = false) ↔ false
+:= subst (a_eq_not_a true) not_true
+
+theorem true_iff_false : (true ↔ false) ↔ false
+:= true_eq_false
+
+theorem false_eq_true : (false = true) ↔ false
+:= subst (a_eq_not_a false) not_false
+
+theorem false_iff_true : (false ↔ true) ↔ false
+:= false_eq_true
+
+theorem a_iff_true (a : Bool) : (a ↔ true) ↔ a
+:= boolext (λ H, eqt_elim H)
+           (λ H, eqt_intro H)
+
+theorem a_iff_false (a : Bool) : (a ↔ false) ↔ ¬ a
+:= boolext (λ H, eqf_elim H)
+           (λ H, eqf_intro H)
+
+add_rewrite a_eq_not_a a_iff_not_a true_eq_false true_iff_false false_eq_true false_iff_true a_iff_true a_iff_false
+
+theorem not_iff (a b : Bool) : ¬ (a ↔ b) ↔ (¬ a ↔ b)
+:= or_elim (em b)
+     (λ Hb, calc (¬ (a ↔ b)) =  (¬ (a ↔ true)) : { eqt_intro Hb }
+                         ...  =  ¬ a            : { a_iff_true a }
+                         ...  = ¬ a ↔ true     : { symm (a_iff_true (¬ a)) }
+                         ...  = ¬ a ↔ b        : { symm (eqt_intro Hb) })
+     (λ Hnb, calc (¬ (a ↔ b)) = (¬ (a ↔ false)) : { eqf_intro Hnb }
+                          ...  = ¬ ¬ a           : { a_iff_false a }
+                          ...  = ¬ a ↔ false    : { symm (a_iff_false (¬ a)) }
+                          ...  = ¬ a ↔ b        : { symm (eqf_intro Hnb) })
+
+theorem not_iff_elim {a b : Bool} (H : ¬ (a ↔ b)) : (¬ a) ↔ b
+:= (not_iff a b) ◂ H
+
 theorem forall_or_distributer {A : TypeU} (p : Bool) (φ : A → Bool) : (∀ x, p ∨ φ x) = (p ∨ ∀ x, φ x)
 := boolext
      (assume H : (∀ x, p ∨ φ x),
@@ -602,9 +677,16 @@ theorem forall_or_distributer {A : TypeU} (p : Bool) (φ : A → Bool) : (∀ x,
               (λ H2 : (∀ x, φ x), or_intror p  (H2 x)))
 
 theorem forall_or_distributel {A : Type} (p : Bool) (φ : A → Bool) : (∀ x, φ x ∨ p) = ((∀ x, φ x) ∨ p)
-:= calc (∀ x, φ x ∨ p) = (∀ x, p ∨ φ x)   : allext (λ x, or_comm (φ x) p)
-                   ...  = (p ∨ ∀ x, φ x)   : forall_or_distributer p φ
-                   ...  = ((∀ x, φ x) ∨ p) : or_comm p (∀ x, φ x)
+:= boolext
+     (assume H : (∀ x, φ x ∨ p),
+        or_elim (em p)
+            (λ Hp  : p,   or_intror (∀ x, φ x) Hp)
+            (λ Hnp : ¬ p, or_introl (take x, resolve2 (H x) Hnp) p))
+     (assume H : (∀ x, φ x) ∨ p,
+        take x,
+            or_elim H
+              (λ H1 : (∀ x, φ x), or_introl (H1 x) p)
+              (λ H2 : p,           or_intror (φ x) H2))
 
 theorem forall_and_distribute {A : TypeU} (φ ψ : A → Bool) : (∀ x, φ x ∧ ψ x) ↔ (∀ x, φ x) ∧ (∀ x, ψ x)
 := boolext
@@ -622,10 +704,6 @@ theorem exists_and_distributer {A : TypeU} (p : Bool) (φ : A → Bool) : (∃ x
         obtain (w : A) (Hw : φ w), from (and_elimr H),
             exists_intro w (and_intro (and_eliml H) Hw))
 
-theorem exists_and_distributel {A : TypeU} (p : Bool) (φ : A → Bool) : (∃ x, φ x ∧ p) ↔ (∃ x, φ x) ∧ p
-:= calc (∃ x, φ x ∧ p) = (∃ x, p ∧ φ x)   : eq_exists_intro (λ x, and_comm (φ x) p)
-                 ...   = (p ∧ (∃ x, φ x)) : exists_and_distributer p φ
-                 ...   = ((∃ x, φ x) ∧ p) : and_comm p (∃ x, φ x)
 
 theorem exists_or_distribute {A : TypeU} (φ ψ : A → Bool) : (∃ x, φ x ∨ ψ x) ↔ (∃ x, φ x) ∨ (∃ x, ψ x)
 := boolext
@@ -643,6 +721,26 @@ theorem exists_or_distribute {A : TypeU} (φ ψ : A → Bool) : (∃ x, φ x ∨
                 obtain (w : A) (Hw : ψ w), from H2,
                     exists_intro w (or_intror (φ w) Hw)))
 
+theorem eq_exists_intro {A : (Type U)} {P Q : A → Bool} (H : ∀ x : A, P x ↔ Q x) : (∃ x : A, P x) ↔ (∃ x : A, Q x)
+:= boolext
+    (assume Hex, obtain w Pw, from Hex,  exists_intro w ((H w) ◂ Pw))
+    (assume Hex, obtain w Qw, from Hex,  exists_intro w ((symm (H w)) ◂ Qw))
+
+theorem not_forall (A : (Type U)) (P : A → Bool) : ¬ (∀ x : A, P x) ↔ (∃ x : A, ¬ P x)
+:= boolext
+    (assume H, refute (λ N : ¬ (∃ x, ¬ P x),
+        absurd (take x, not_not_elim (not_exists_elim N x)) H))
+    (assume (H : ∃ x, ¬ P x) (N : ∀ x, P x),
+        obtain w Hw, from H,
+           absurd (N w) Hw)
+
+theorem not_forall_elim {A : (Type U)} {P : A → Bool} (H : ¬ (∀ x : A, P x)) : ∃ x : A, ¬ P x
+:= (not_forall A P) ◂ H
+
+theorem exists_and_distributel {A : TypeU} (p : Bool) (φ : A → Bool) : (∃ x, φ x ∧ p) ↔ (∃ x, φ x) ∧ p
+:= calc (∃ x, φ x ∧ p) = (∃ x, p ∧ φ x)   : eq_exists_intro (λ x, and_comm (φ x) p)
+                 ...   = (p ∧ (∃ x, φ x)) : exists_and_distributer p φ
+                 ...   = ((∃ x, φ x) ∧ p) : and_comm p (∃ x, φ x)
 
 theorem exists_imp_distribute {A : TypeU} (φ ψ : A → Bool) : (∃ x, φ x → ψ x) ↔ ((∀ x, φ x) → (∃ x, ψ x))
 := calc (∃ x, φ x → ψ x) = (∃ x, ¬ φ x ∨ ψ x)           : eq_exists_intro (λ x, imp_or (φ x) (ψ x))
@@ -650,25 +748,73 @@ theorem exists_imp_distribute {A : TypeU} (φ ψ : A → Bool) : (∃ x, φ x 
                      ...   = ¬ (∀ x, φ x) ∨ (∃ x, ψ x)   : { symm (not_forall A φ) }
                      ...   = (∀ x, φ x) → (∃ x, ψ x)     : symm (imp_or _ _)
 
--- If a function space is non-empty, then for every 'a' in the domain, the range (B a) is not empty
-theorem nonempty_range {A : TypeU} {B : A → TypeU} (H : nonempty (∀ x, B x)) (a : A) : nonempty (B a)
-:= refute (λ N : ¬ nonempty (B a),
-     let s1 : ¬ ∃ x : B a, true       := N,
-         s2 : ∀ x : B a, false        := not_exists_elim s1,
-         s3 : ∃ y : (∀ x, B x), true := H
-     in obtain (w : (∀ x, B x)) (Hw : true), from s3,
-           let s4 : B a := w a
-           in s2 s4)
+theorem forall_uninhabited {A : (Type U)} {B : A → Bool} (H : ¬ inhabited A) : ∀ x, B x
+:= refute (λ N : ¬ (∀ x, B x),
+      obtain w Hw, from not_forall_elim N,
+         absurd (inhabited_intro w) H)
+
+theorem allext {A : (Type U)} {B C : A → Bool} (H : ∀ x : A, B x = C x) : (∀ x : A, B x) = (∀ x : A, C x)
+:= boolext
+     (assume Hl, take x, (H x) ◂ (Hl x))
+     (assume Hr, take x, (symm (H x)) ◂ (Hr x))
+
+-- Up to this point, we proved all theorems using just reflexivity, substitution and case (proof by cases)
+
+-- Function extensionality
+axiom funext {A : (Type U)} {B : A → (Type U)} {f g : ∀ x : A, B x} (H : ∀ x : A, f x = g x) : f = g
+
+-- Eta is a consequence of function extensionality
+theorem eta {A : TypeU} {B : A → TypeU} (f : ∀ x : A, B x) : (λ x : A, f x) = f
+:= funext (λ x : A, refl (f x))
+
+-- Epsilon (Hilbert's operator)
+variable eps {A : TypeU} (H : inhabited A) (P : A → Bool) : A
+alias ε : eps
+axiom eps_ax {A : TypeU} (H : inhabited A) {P : A → Bool} (a : A) : P a → P (ε H P)
+
+theorem eps_th {A : TypeU} {P : A → Bool} (a : A) : P a → P (ε (inhabited_intro a) P)
+:= assume H : P a, @eps_ax A (inhabited_intro a) P a H
+
+theorem eps_singleton {A : TypeU} (H : inhabited A) (a : A) : ε H (λ x, x = a) = a
+:= let P         :=  λ x, x = a,
+       Ha : P a  :=  refl a
+   in eps_ax H a Ha
+
+-- A function space (∀ x : A, B x) is inhabited if forall a : A, we have inhabited (B a)
+theorem inhabited_fun {A : TypeU} {B : A → TypeU} (Hn : ∀ a, inhabited (B a)) : inhabited (∀ x, B x)
+:= inhabited_intro (λ x, ε (Hn x) (λ y, true))
+
+theorem exists_to_eps {A : TypeU} {P : A → Bool} (H : ∃ x, P x) : P (ε (inhabited_ex_intro H) P)
+:= obtain (w : A) (Hw : P w), from H,
+      eps_ax (inhabited_ex_intro H) w Hw
+
+theorem axiom_of_choice {A : TypeU} {B : A → TypeU} {R : ∀ x : A, B x → Bool} (H : ∀ x, ∃ y, R x y) : ∃ f, ∀ x, R x (f x)
+:= exists_intro
+      (λ x, ε (inhabited_ex_intro (H x)) (λ y, R x y)) -- witness for f
+      (λ x, exists_to_eps (H x))                      -- proof that witness satisfies ∀ x, R x (f x)
+
+theorem skolem_th {A : TypeU} {B : A → TypeU} {P : ∀ x : A, B x → Bool} :
+        (∀ x, ∃ y, P x y) ↔ ∃ f, (∀ x, P x (f x))
+:= iff_intro
+      (λ H : (∀ x, ∃ y, P x y), axiom_of_choice H)
+      (λ H : (∃ f, (∀ x, P x (f x))),
+             take x, obtain (fw : ∀ x, B x) (Hw : ∀ x, P x (fw x)), from H,
+                  exists_intro (fw x) (Hw x))
+
+-- if-then-else expression, we define it using Hilbert's operator
+definition ite {A : TypeU} (c : Bool) (a b : A) : A
+:= ε (inhabited_intro a) (λ r, (c → r = a) ∧ (¬ c → r = b))
+notation 45 if _ then _ else _ : ite
 
 theorem if_true {A : TypeU} (a b : A) : (if true then a else b) = a
-:= calc (if true then a else b) = ε (nonempty_intro a) (λ r, (true → r = a) ∧ (¬ true → r = b)) : refl (if true then a else b)
-                           ...  = ε (nonempty_intro a) (λ r, r = a)                               : by simp
-                           ...  = a        : eps_singleton (nonempty_intro a) a
+:= calc (if true then a else b) = ε (inhabited_intro a) (λ r, (true → r = a) ∧ (¬ true → r = b)) : refl (if true then a else b)
+                           ...  = ε (inhabited_intro a) (λ r, r = a)                               : by simp
+                           ...  = a        : eps_singleton (inhabited_intro a) a
 
 theorem if_false {A : TypeU} (a b : A) : (if false then a else b) = b
-:= calc (if false then a else b) = ε (nonempty_intro a) (λ r, (false → r = a) ∧ (¬ false → r = b)) : refl (if false then a else b)
-                            ...  = ε (nonempty_intro a) (λ r, r = b)              : by simp
-                            ...  = b                                              : eps_singleton (nonempty_intro a) b
+:= calc (if false then a else b) = ε (inhabited_intro a) (λ r, (false → r = a) ∧ (¬ false → r = b)) : refl (if false then a else b)
+                            ...  = ε (inhabited_intro a) (λ r, r = b)              : by simp
+                            ...  = b                                              : eps_singleton (inhabited_intro a) b
 
 theorem if_a_a {A : TypeU} (c : Bool) (a: A) : (if c then a else a) = a
 := or_elim (em c)
@@ -732,4 +878,17 @@ set_opaque not     true
 set_opaque or      true
 set_opaque and     true
 set_opaque implies true
-set_opaque ite     true
\ No newline at end of file
+set_opaque ite     true
+set_opaque eq      true
+
+definition injective {A B : (Type U)} (f : A → B)  := ∀ x1 x2, f x1 = f x2 → x1 = x2
+definition non_surjective {A B : (Type U)} (f : A → B) := ∃ y, ∀ x, ¬ f x = y
+
+-- The set of individuals, we need to assert the existence of one infinite set
+variable ind : Type
+-- ind is infinite, i.e., there is a function f s.t. f is injective, and not surjective
+axiom infinity : ∃ f : ind → ind, injective f ∧ non_surjective f
+
+-- Proof irrelevance, this is true in the set theoretic model we have for Lean
+-- It is also useful when we introduce casts
+axiom proof_irrel {a : Bool} (H1 H2 : a) : H1 = H2
diff --git a/src/builtin/obj/Int.olean b/src/builtin/obj/Int.olean
index 7c50c8c1d..f2f432c9b 100644
Binary files a/src/builtin/obj/Int.olean and b/src/builtin/obj/Int.olean differ
diff --git a/src/builtin/obj/Nat.olean b/src/builtin/obj/Nat.olean
index 9559a315f..99a10bf44 100644
Binary files a/src/builtin/obj/Nat.olean and b/src/builtin/obj/Nat.olean differ
diff --git a/src/builtin/obj/cast.olean b/src/builtin/obj/cast.olean
index 47d0db100..431b4fac1 100644
Binary files a/src/builtin/obj/cast.olean and b/src/builtin/obj/cast.olean differ
diff --git a/src/builtin/obj/heq.olean b/src/builtin/obj/heq.olean
index b32c74f30..2f68811a5 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 98684cbb4..0b37c6f80 100644
Binary files a/src/builtin/obj/kernel.olean and b/src/builtin/obj/kernel.olean differ
diff --git a/src/frontends/lean/parser_cmds.cpp b/src/frontends/lean/parser_cmds.cpp
index 1236e0b48..8224723c6 100644
--- a/src/frontends/lean/parser_cmds.cpp
+++ b/src/frontends/lean/parser_cmds.cpp
@@ -275,7 +275,7 @@ void parser_imp::parse_eval() {
     next();
     expr v = m_elaborator(parse_expr()).first;
     normalizer norm(m_env);
-    expr r = norm(v, context(), true);
+    expr r = norm(v);
     regular(m_io_state) << r << endl;
 }
 
diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index 1c2566706..b2692c635 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -927,9 +927,12 @@ class pp_fn {
             } else {
                 body_sep = comma();
             }
-            expr domain0 = nested[0].second;
-            if (std::all_of(nested.begin() + 1, nested.end(), [&](std::pair<name, expr> const & p) { return p.second == domain0; }) && !implicit_args) {
+            if (!nested.empty() &&
+                std::all_of(nested.begin() + 1, nested.end(), [&](std::pair<name, expr> const & p) {
+                        return p.second == nested[0].second; }) &&
+                !implicit_args) {
                 // Domain of all binders is the same
+                expr domain0    = nested[0].second;
                 format names    = pp_bnames(nested.begin(), nested.end(), false);
                 result p_domain = pp_scoped_child(domain0, depth);
                 result p_body   = pp_scoped_child(b, depth);
diff --git a/src/kernel/kernel.cpp b/src/kernel/kernel.cpp
index d7dd91407..fcfbddd9a 100644
--- a/src/kernel/kernel.cpp
+++ b/src/kernel/kernel.cpp
@@ -21,100 +21,25 @@ expr const TypeU1 = Type(u_lvl+1);
 
 // =======================================
 // Boolean Type
-expr const Bool = mk_Bool();
+expr const Bool  = mk_Bool();
+expr const True  = mk_true();
+expr const False = mk_false();
 expr mk_bool_type() { return mk_Bool(); }
 bool is_bool(expr const & t) { return is_Bool(t); }
 // =======================================
 
-// =======================================
-// Boolean values True and False
-static name g_true_name("true");
-static name g_false_name("false");
-static name g_true_u_name("\u22A4"); // ⊤
-static name g_false_u_name("\u22A5"); // ⊥
-/**
-   \brief Semantic attachments for Boolean values.
-*/
-class bool_value_value : public value {
-    bool m_val;
-public:
-    bool_value_value(bool v):m_val(v) {}
-    virtual ~bool_value_value() {}
-    virtual expr get_type() const { return Bool; }
-    virtual name get_name() const { return m_val ? g_true_name : g_false_name; }
-    virtual name get_unicode_name() const { return m_val ? g_true_u_name : g_false_u_name; }
-    // LCOV_EXCL_START
-    virtual bool operator==(value const & other) const {
-        // This method is unreachable because there is only one copy of True and False in the system,
-        // and they have different hashcodes.
-        bool_value_value const * _other = dynamic_cast<bool_value_value const*>(&other);
-        return _other && _other->m_val == m_val;
-    }
-    // LCOV_EXCL_STOP
-    virtual void write(serializer & s) const { s << (m_val ? "true" : "false"); }
-    bool get_val() const { return m_val; }
-};
-expr const True  = mk_value(*(new bool_value_value(true)));
-expr const False = mk_value(*(new bool_value_value(false)));
-static register_builtin_fn true_blt("true", []() { return  True; });
-static register_builtin_fn false_blt("false", []() { return False; });
-static value::register_deserializer_fn true_ds("true", [](deserializer & ) { return True; });
-static value::register_deserializer_fn false_ds("false", [](deserializer & ) { return False; });
-
 expr mk_bool_value(bool v) {
     return v ? True : False;
 }
 bool is_bool_value(expr const & e) {
-    return is_value(e) && dynamic_cast<bool_value_value const *>(&to_value(e)) != nullptr;
+    return is_true(e) || is_false(e);
 }
 bool to_bool(expr const & e) {
     lean_assert(is_bool_value(e));
-    return static_cast<bool_value_value const &>(to_value(e)).get_val();
-}
-bool is_true(expr const & e) {
-    return is_bool_value(e) && to_bool(e);
-}
-bool is_false(expr const & e) {
-    return is_bool_value(e) && !to_bool(e);
+    return e == True;
 }
 // =======================================
 
-// =======================================
-// Equality
-static name   g_eq_name("eq");
-static format g_eq_fmt(g_eq_name);
-/**
-   \brief Semantic attachment for if-then-else operator with type
-   <code>Pi (A : Type), Bool -> A -> A -> A</code>
-*/
-class eq_fn_value : public value {
-    expr m_type;
-    static expr mk_type() {
-        expr A    = Const("A");
-        // Pi (A: TypeU), A -> A -> Bool
-        return Pi({A, TypeU}, (A >> (A >> Bool)));
-    }
-public:
-    eq_fn_value():m_type(mk_type()) {}
-    virtual ~eq_fn_value() {}
-    virtual expr get_type() const { return m_type; }
-    virtual name get_name() const { return g_eq_name; }
-    virtual optional<expr> normalize(unsigned num_args, expr const * args) const {
-        if (num_args == 4 && is_value(args[2]) && is_value(args[3]) && typeid(to_value(args[2])) == typeid(to_value(args[3]))) {
-            return some_expr(mk_bool_value(args[2] == args[3]));
-        } else {
-            return none_expr();
-        }
-    }
-    virtual void write(serializer & s) const { s << "eq"; }
-};
-MK_BUILTIN(eq_fn, eq_fn_value);
-MK_IS_BUILTIN(is_eq_fn, mk_eq_fn());
-static register_builtin_fn eq_blt("eq", []() { return mk_eq_fn(); });
-static value::register_deserializer_fn eq_ds("eq", [](deserializer & ) { return mk_eq_fn(); });
-// =======================================
-
-
 void import_kernel(environment const & env, io_state const & ios) {
     env->import("kernel", ios);
 }
diff --git a/src/kernel/kernel.h b/src/kernel/kernel.h
index 9c6edbd6b..b142288ce 100644
--- a/src/kernel/kernel.h
+++ b/src/kernel/kernel.h
@@ -29,15 +29,6 @@ bool is_bool_value(expr const & e);
     \pre is_bool_value(e)
 */
 bool to_bool(expr const & e);
-/** \brief Return true iff \c e is the Lean true value. */
-bool is_true(expr const & e);
-/** \brief Return true iff \c e is the Lean false value. */
-bool is_false(expr const & e);
-
-expr mk_eq_fn();
-bool is_eq_fn(expr const & e);
-inline expr mk_eq(expr const & A, expr const & lhs, expr const & rhs) { return mk_app(mk_eq_fn(), A, lhs, rhs); }
-inline bool is_eq(expr const & e) { return is_app(e) && is_eq_fn(arg(e, 0)) && num_args(e) == 4; }
 
 inline expr Implies(expr const & e1, expr const & e2) { return mk_implies(e1, e2); }
 inline expr And(expr const & e1, expr const & e2) { return mk_and(e1, e2); }
diff --git a/src/kernel/kernel_decls.cpp b/src/kernel/kernel_decls.cpp
index 66cf7a16e..db1b56b45 100644
--- a/src/kernel/kernel_decls.cpp
+++ b/src/kernel/kernel_decls.cpp
@@ -8,81 +8,82 @@ Released under Apache 2.0 license as described in the file LICENSE.
 namespace lean {
 MK_CONSTANT(TypeU, name("TypeU"));
 MK_CONSTANT(Bool, name("Bool"));
+MK_CONSTANT(heq_fn, name("heq"));
+MK_CONSTANT(hrefl_fn, name("hrefl"));
+MK_CONSTANT(eq_fn, name("eq"));
+MK_CONSTANT(refl_fn, name("refl"));
+MK_CONSTANT(heq_eq_fn, name("heq_eq"));
+MK_CONSTANT(true, name("true"));
+MK_CONSTANT(trivial, name("trivial"));
+MK_CONSTANT(false, name("false"));
 MK_CONSTANT(not_fn, name("not"));
 MK_CONSTANT(or_fn, name("or"));
 MK_CONSTANT(and_fn, name("and"));
 MK_CONSTANT(implies_fn, name("implies"));
 MK_CONSTANT(neq_fn, name("neq"));
+MK_CONSTANT(a_neq_a_elim_fn, name("a_neq_a_elim"));
 MK_CONSTANT(iff_fn, name("iff"));
-MK_CONSTANT(exists_fn, name("exists"));
-MK_CONSTANT(nonempty_fn, name("nonempty"));
-MK_CONSTANT(nonempty_intro_fn, name("nonempty_intro"));
 MK_CONSTANT(em_fn, name("em"));
-MK_CONSTANT(case_fn, name("case"));
-MK_CONSTANT(refl_fn, name("refl"));
-MK_CONSTANT(subst_fn, name("subst"));
-MK_CONSTANT(funext_fn, name("funext"));
-MK_CONSTANT(allext_fn, name("allext"));
-MK_CONSTANT(eps_fn, name("eps"));
-MK_CONSTANT(eps_ax_fn, name("eps_ax"));
-MK_CONSTANT(proof_irrel_fn, name("proof_irrel"));
-MK_CONSTANT(substp_fn, name("substp"));
-MK_CONSTANT(eps_th_fn, name("eps_th"));
-MK_CONSTANT(eps_singleton_fn, name("eps_singleton"));
-MK_CONSTANT(nonempty_fun_fn, name("nonempty_fun"));
-MK_CONSTANT(ite_fn, name("ite"));
 MK_CONSTANT(not_intro_fn, name("not_intro"));
-MK_CONSTANT(eta_fn, name("eta"));
-MK_CONSTANT(trivial, name("trivial"));
 MK_CONSTANT(absurd_fn, name("absurd"));
-MK_CONSTANT(eqmp_fn, name("eqmp"));
-MK_CONSTANT(boolcomplete_fn, name("boolcomplete"));
+MK_CONSTANT(exists_fn, name("exists"));
+MK_CONSTANT(case_fn, name("case"));
 MK_CONSTANT(false_elim_fn, name("false_elim"));
-MK_CONSTANT(imp_trans_fn, name("imp_trans"));
-MK_CONSTANT(imp_eq_trans_fn, name("imp_eq_trans"));
-MK_CONSTANT(eq_imp_trans_fn, name("eq_imp_trans"));
-MK_CONSTANT(not_not_eq_fn, name("not_not_eq"));
-MK_CONSTANT(not_not_elim_fn, name("not_not_elim"));
 MK_CONSTANT(mt_fn, name("mt"));
 MK_CONSTANT(contrapos_fn, name("contrapos"));
 MK_CONSTANT(absurd_elim_fn, name("absurd_elim"));
-MK_CONSTANT(not_imp_eliml_fn, name("not_imp_eliml"));
-MK_CONSTANT(not_imp_elimr_fn, name("not_imp_elimr"));
-MK_CONSTANT(resolve1_fn, name("resolve1"));
-MK_CONSTANT(and_intro_fn, name("and_intro"));
-MK_CONSTANT(and_eliml_fn, name("and_eliml"));
-MK_CONSTANT(and_elimr_fn, name("and_elimr"));
 MK_CONSTANT(or_introl_fn, name("or_introl"));
 MK_CONSTANT(or_intror_fn, name("or_intror"));
-MK_CONSTANT(or_elim_fn, name("or_elim"));
-MK_CONSTANT(refute_fn, name("refute"));
+MK_CONSTANT(boolcomplete_fn, name("boolcomplete"));
+MK_CONSTANT(boolcomplete_swapped_fn, name("boolcomplete_swapped"));
+MK_CONSTANT(resolve1_fn, name("resolve1"));
+MK_CONSTANT(subst_fn, name("subst"));
+MK_CONSTANT(substp_fn, name("substp"));
 MK_CONSTANT(symm_fn, name("symm"));
-MK_CONSTANT(eqmpr_fn, name("eqmpr"));
 MK_CONSTANT(trans_fn, name("trans"));
+MK_CONSTANT(congr1_fn, name("congr1"));
+MK_CONSTANT(congr2_fn, name("congr2"));
+MK_CONSTANT(congr_fn, name("congr"));
+MK_CONSTANT(true_ne_false, name("true_ne_false"));
+MK_CONSTANT(absurd_not_true_fn, name("absurd_not_true"));
+MK_CONSTANT(not_false_trivial, name("not_false_trivial"));
+MK_CONSTANT(eqmp_fn, name("eqmp"));
+MK_CONSTANT(eqmpr_fn, name("eqmpr"));
+MK_CONSTANT(imp_trans_fn, name("imp_trans"));
+MK_CONSTANT(imp_eq_trans_fn, name("imp_eq_trans"));
+MK_CONSTANT(eq_imp_trans_fn, name("eq_imp_trans"));
+MK_CONSTANT(to_eq_fn, name("to_eq"));
+MK_CONSTANT(to_heq_fn, name("to_heq"));
+MK_CONSTANT(iff_eliml_fn, name("iff_eliml"));
+MK_CONSTANT(iff_elimr_fn, name("iff_elimr"));
 MK_CONSTANT(ne_symm_fn, name("ne_symm"));
 MK_CONSTANT(eq_ne_trans_fn, name("eq_ne_trans"));
 MK_CONSTANT(ne_eq_trans_fn, name("ne_eq_trans"));
 MK_CONSTANT(eqt_elim_fn, name("eqt_elim"));
 MK_CONSTANT(eqf_elim_fn, name("eqf_elim"));
-MK_CONSTANT(congr1_fn, name("congr1"));
-MK_CONSTANT(congr2_fn, name("congr2"));
-MK_CONSTANT(congr_fn, name("congr"));
-MK_CONSTANT(exists_elim_fn, name("exists_elim"));
-MK_CONSTANT(exists_intro_fn, name("exists_intro"));
-MK_CONSTANT(nonempty_elim_fn, name("nonempty_elim"));
-MK_CONSTANT(nonempty_ex_intro_fn, name("nonempty_ex_intro"));
-MK_CONSTANT(exists_to_eps_fn, name("exists_to_eps"));
-MK_CONSTANT(axiom_of_choice_fn, name("axiom_of_choice"));
+MK_CONSTANT(heqt_elim_fn, name("heqt_elim"));
+MK_CONSTANT(not_true, name("not_true"));
+MK_CONSTANT(not_false, name("not_false"));
+MK_CONSTANT(not_not_eq_fn, name("not_not_eq"));
+MK_CONSTANT(not_neq_fn, name("not_neq"));
+MK_CONSTANT(not_neq_elim_fn, name("not_neq_elim"));
+MK_CONSTANT(not_not_elim_fn, name("not_not_elim"));
+MK_CONSTANT(not_imp_eliml_fn, name("not_imp_eliml"));
+MK_CONSTANT(not_imp_elimr_fn, name("not_imp_elimr"));
+MK_CONSTANT(and_intro_fn, name("and_intro"));
+MK_CONSTANT(and_eliml_fn, name("and_eliml"));
+MK_CONSTANT(and_elimr_fn, name("and_elimr"));
+MK_CONSTANT(or_elim_fn, name("or_elim"));
+MK_CONSTANT(refute_fn, name("refute"));
 MK_CONSTANT(boolext_fn, name("boolext"));
 MK_CONSTANT(iff_intro_fn, name("iff_intro"));
-MK_CONSTANT(iff_eliml_fn, name("iff_eliml"));
-MK_CONSTANT(iff_elimr_fn, name("iff_elimr"));
-MK_CONSTANT(skolem_th_fn, name("skolem_th"));
 MK_CONSTANT(eqt_intro_fn, name("eqt_intro"));
 MK_CONSTANT(eqf_intro_fn, name("eqf_intro"));
-MK_CONSTANT(neq_elim_fn, name("neq_elim"));
+MK_CONSTANT(a_neq_a_fn, name("a_neq_a"));
 MK_CONSTANT(eq_id_fn, name("eq_id"));
 MK_CONSTANT(iff_id_fn, name("iff_id"));
+MK_CONSTANT(neq_elim_fn, name("neq_elim"));
+MK_CONSTANT(neq_to_not_eq_fn, name("neq_to_not_eq"));
 MK_CONSTANT(left_comm_fn, name("left_comm"));
 MK_CONSTANT(or_comm_fn, name("or_comm"));
 MK_CONSTANT(or_assoc_fn, name("or_assoc"));
@@ -93,6 +94,7 @@ MK_CONSTANT(or_truel_fn, name("or_truel"));
 MK_CONSTANT(or_truer_fn, name("or_truer"));
 MK_CONSTANT(or_tauto_fn, name("or_tauto"));
 MK_CONSTANT(or_left_comm_fn, name("or_left_comm"));
+MK_CONSTANT(resolve2_fn, name("resolve2"));
 MK_CONSTANT(and_comm_fn, name("and_comm"));
 MK_CONSTANT(and_id_fn, name("and_id"));
 MK_CONSTANT(and_assoc_fn, name("and_assoc"));
@@ -108,29 +110,21 @@ MK_CONSTANT(imp_falser_fn, name("imp_falser"));
 MK_CONSTANT(imp_falsel_fn, name("imp_falsel"));
 MK_CONSTANT(imp_id_fn, name("imp_id"));
 MK_CONSTANT(imp_or_fn, name("imp_or"));
-MK_CONSTANT(not_true, name("not_true"));
-MK_CONSTANT(not_false, name("not_false"));
-MK_CONSTANT(not_neq_fn, name("not_neq"));
-MK_CONSTANT(not_neq_elim_fn, name("not_neq_elim"));
-MK_CONSTANT(not_and_fn, name("not_and"));
-MK_CONSTANT(not_and_elim_fn, name("not_and_elim"));
-MK_CONSTANT(not_or_fn, name("not_or"));
-MK_CONSTANT(not_or_elim_fn, name("not_or_elim"));
-MK_CONSTANT(not_iff_fn, name("not_iff"));
-MK_CONSTANT(not_iff_elim_fn, name("not_iff_elim"));
-MK_CONSTANT(not_implies_fn, name("not_implies"));
-MK_CONSTANT(not_implies_elim_fn, name("not_implies_elim"));
 MK_CONSTANT(not_congr_fn, name("not_congr"));
-MK_CONSTANT(exists_rem_fn, name("exists_rem"));
-MK_CONSTANT(forall_rem_fn, name("forall_rem"));
-MK_CONSTANT(eq_exists_intro_fn, name("eq_exists_intro"));
-MK_CONSTANT(not_forall_fn, name("not_forall"));
-MK_CONSTANT(not_forall_elim_fn, name("not_forall_elim"));
+MK_CONSTANT(exists_elim_fn, name("exists_elim"));
+MK_CONSTANT(exists_intro_fn, name("exists_intro"));
 MK_CONSTANT(not_exists_fn, name("not_exists"));
 MK_CONSTANT(not_exists_elim_fn, name("not_exists_elim"));
 MK_CONSTANT(exists_unfold1_fn, name("exists_unfold1"));
 MK_CONSTANT(exists_unfold2_fn, name("exists_unfold2"));
 MK_CONSTANT(exists_unfold_fn, name("exists_unfold"));
+MK_CONSTANT(inhabited_fn, name("inhabited"));
+MK_CONSTANT(inhabited_intro_fn, name("inhabited_intro"));
+MK_CONSTANT(inhabited_elim_fn, name("inhabited_elim"));
+MK_CONSTANT(inhabited_ex_intro_fn, name("inhabited_ex_intro"));
+MK_CONSTANT(inhabited_range_fn, name("inhabited_range"));
+MK_CONSTANT(exists_rem_fn, name("exists_rem"));
+MK_CONSTANT(forall_rem_fn, name("forall_rem"));
 MK_CONSTANT(imp_congrr_fn, name("imp_congrr"));
 MK_CONSTANT(imp_congrl_fn, name("imp_congrl"));
 MK_CONSTANT(imp_congr_fn, name("imp_congr"));
@@ -140,14 +134,45 @@ MK_CONSTANT(or_congr_fn, name("or_congr"));
 MK_CONSTANT(and_congrr_fn, name("and_congrr"));
 MK_CONSTANT(and_congrl_fn, name("and_congrl"));
 MK_CONSTANT(and_congr_fn, name("and_congr"));
+MK_CONSTANT(not_and_fn, name("not_and"));
+MK_CONSTANT(not_and_elim_fn, name("not_and_elim"));
+MK_CONSTANT(not_or_fn, name("not_or"));
+MK_CONSTANT(not_or_elim_fn, name("not_or_elim"));
+MK_CONSTANT(not_implies_fn, name("not_implies"));
+MK_CONSTANT(not_implies_elim_fn, name("not_implies_elim"));
+MK_CONSTANT(a_eq_not_a_fn, name("a_eq_not_a"));
+MK_CONSTANT(a_iff_not_a_fn, name("a_iff_not_a"));
+MK_CONSTANT(true_eq_false, name("true_eq_false"));
+MK_CONSTANT(true_iff_false, name("true_iff_false"));
+MK_CONSTANT(false_eq_true, name("false_eq_true"));
+MK_CONSTANT(false_iff_true, name("false_iff_true"));
+MK_CONSTANT(a_iff_true_fn, name("a_iff_true"));
+MK_CONSTANT(a_iff_false_fn, name("a_iff_false"));
+MK_CONSTANT(not_iff_fn, name("not_iff"));
+MK_CONSTANT(not_iff_elim_fn, name("not_iff_elim"));
 MK_CONSTANT(forall_or_distributer_fn, name("forall_or_distributer"));
 MK_CONSTANT(forall_or_distributel_fn, name("forall_or_distributel"));
 MK_CONSTANT(forall_and_distribute_fn, name("forall_and_distribute"));
 MK_CONSTANT(exists_and_distributer_fn, name("exists_and_distributer"));
-MK_CONSTANT(exists_and_distributel_fn, name("exists_and_distributel"));
 MK_CONSTANT(exists_or_distribute_fn, name("exists_or_distribute"));
+MK_CONSTANT(eq_exists_intro_fn, name("eq_exists_intro"));
+MK_CONSTANT(not_forall_fn, name("not_forall"));
+MK_CONSTANT(not_forall_elim_fn, name("not_forall_elim"));
+MK_CONSTANT(exists_and_distributel_fn, name("exists_and_distributel"));
 MK_CONSTANT(exists_imp_distribute_fn, name("exists_imp_distribute"));
-MK_CONSTANT(nonempty_range_fn, name("nonempty_range"));
+MK_CONSTANT(forall_uninhabited_fn, name("forall_uninhabited"));
+MK_CONSTANT(allext_fn, name("allext"));
+MK_CONSTANT(funext_fn, name("funext"));
+MK_CONSTANT(eta_fn, name("eta"));
+MK_CONSTANT(eps_fn, name("eps"));
+MK_CONSTANT(eps_ax_fn, name("eps_ax"));
+MK_CONSTANT(eps_th_fn, name("eps_th"));
+MK_CONSTANT(eps_singleton_fn, name("eps_singleton"));
+MK_CONSTANT(inhabited_fun_fn, name("inhabited_fun"));
+MK_CONSTANT(exists_to_eps_fn, name("exists_to_eps"));
+MK_CONSTANT(axiom_of_choice_fn, name("axiom_of_choice"));
+MK_CONSTANT(skolem_th_fn, name("skolem_th"));
+MK_CONSTANT(ite_fn, name("ite"));
 MK_CONSTANT(if_true_fn, name("if_true"));
 MK_CONSTANT(if_false_fn, name("if_false"));
 MK_CONSTANT(if_a_a_fn, name("if_a_a"));
@@ -157,4 +182,9 @@ MK_CONSTANT(if_imp_else_fn, name("if_imp_else"));
 MK_CONSTANT(app_if_distribute_fn, name("app_if_distribute"));
 MK_CONSTANT(eq_if_distributer_fn, name("eq_if_distributer"));
 MK_CONSTANT(eq_if_distributel_fn, name("eq_if_distributel"));
+MK_CONSTANT(injective_fn, name("injective"));
+MK_CONSTANT(non_surjective_fn, name("non_surjective"));
+MK_CONSTANT(ind, name("ind"));
+MK_CONSTANT(infinity, name("infinity"));
+MK_CONSTANT(proof_irrel_fn, name("proof_irrel"));
 }
diff --git a/src/kernel/kernel_decls.h b/src/kernel/kernel_decls.h
index 2ee04c003..4ff9b571b 100644
--- a/src/kernel/kernel_decls.h
+++ b/src/kernel/kernel_decls.h
@@ -9,6 +9,29 @@ expr mk_TypeU();
 bool is_TypeU(expr const & e);
 expr mk_Bool();
 bool is_Bool(expr const & e);
+expr mk_heq_fn();
+bool is_heq_fn(expr const & e);
+inline bool is_heq(expr const & e) { return is_app(e) && is_heq_fn(arg(e, 0)) && num_args(e) == 5; }
+inline expr mk_heq(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_heq_fn(), e1, e2, e3, e4}); }
+expr mk_hrefl_fn();
+bool is_hrefl_fn(expr const & e);
+inline expr mk_hrefl_th(expr const & e1, expr const & e2) { return mk_app({mk_hrefl_fn(), e1, e2}); }
+expr mk_eq_fn();
+bool is_eq_fn(expr const & e);
+inline bool is_eq(expr const & e) { return is_app(e) && is_eq_fn(arg(e, 0)) && num_args(e) == 4; }
+inline expr mk_eq(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_eq_fn(), e1, e2, e3}); }
+expr mk_refl_fn();
+bool is_refl_fn(expr const & e);
+inline expr mk_refl_th(expr const & e1, expr const & e2) { return mk_app({mk_refl_fn(), e1, e2}); }
+expr mk_heq_eq_fn();
+bool is_heq_eq_fn(expr const & e);
+inline expr mk_heq_eq_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_heq_eq_fn(), e1, e2, e3}); }
+expr mk_true();
+bool is_true(expr const & e);
+expr mk_trivial();
+bool is_trivial(expr const & e);
+expr mk_false();
+bool is_false(expr const & e);
 expr mk_not_fn();
 bool is_not_fn(expr const & e);
 inline bool is_not(expr const & e) { return is_app(e) && is_not_fn(arg(e, 0)) && num_args(e) == 2; }
@@ -29,100 +52,32 @@ expr mk_neq_fn();
 bool is_neq_fn(expr const & e);
 inline bool is_neq(expr const & e) { return is_app(e) && is_neq_fn(arg(e, 0)) && num_args(e) == 4; }
 inline expr mk_neq(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_neq_fn(), e1, e2, e3}); }
+expr mk_a_neq_a_elim_fn();
+bool is_a_neq_a_elim_fn(expr const & e);
+inline expr mk_a_neq_a_elim_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_a_neq_a_elim_fn(), e1, e2, e3}); }
 expr mk_iff_fn();
 bool is_iff_fn(expr const & e);
 inline bool is_iff(expr const & e) { return is_app(e) && is_iff_fn(arg(e, 0)) && num_args(e) == 3; }
 inline expr mk_iff(expr const & e1, expr const & e2) { return mk_app({mk_iff_fn(), e1, e2}); }
+expr mk_em_fn();
+bool is_em_fn(expr const & e);
+inline expr mk_em_th(expr const & e1) { return mk_app({mk_em_fn(), e1}); }
+expr mk_not_intro_fn();
+bool is_not_intro_fn(expr const & e);
+inline expr mk_not_intro_th(expr const & e1, expr const & e2) { return mk_app({mk_not_intro_fn(), e1, e2}); }
+expr mk_absurd_fn();
+bool is_absurd_fn(expr const & e);
+inline expr mk_absurd_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_absurd_fn(), e1, e2, e3}); }
 expr mk_exists_fn();
 bool is_exists_fn(expr const & e);
 inline bool is_exists(expr const & e) { return is_app(e) && is_exists_fn(arg(e, 0)) && num_args(e) == 3; }
 inline expr mk_exists(expr const & e1, expr const & e2) { return mk_app({mk_exists_fn(), e1, e2}); }
-expr mk_nonempty_fn();
-bool is_nonempty_fn(expr const & e);
-inline bool is_nonempty(expr const & e) { return is_app(e) && is_nonempty_fn(arg(e, 0)) && num_args(e) == 2; }
-inline expr mk_nonempty(expr const & e1) { return mk_app({mk_nonempty_fn(), e1}); }
-expr mk_nonempty_intro_fn();
-bool is_nonempty_intro_fn(expr const & e);
-inline expr mk_nonempty_intro_th(expr const & e1, expr const & e2) { return mk_app({mk_nonempty_intro_fn(), e1, e2}); }
-expr mk_em_fn();
-bool is_em_fn(expr const & e);
-inline expr mk_em_th(expr const & e1) { return mk_app({mk_em_fn(), e1}); }
 expr mk_case_fn();
 bool is_case_fn(expr const & e);
 inline expr mk_case_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_case_fn(), e1, e2, e3, e4}); }
-expr mk_refl_fn();
-bool is_refl_fn(expr const & e);
-inline expr mk_refl_th(expr const & e1, expr const & e2) { return mk_app({mk_refl_fn(), e1, e2}); }
-expr mk_subst_fn();
-bool is_subst_fn(expr const & e);
-inline expr mk_subst_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_subst_fn(), e1, e2, e3, e4, e5, e6}); }
-expr mk_funext_fn();
-bool is_funext_fn(expr const & e);
-inline expr mk_funext_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_funext_fn(), e1, e2, e3, e4, e5}); }
-expr mk_allext_fn();
-bool is_allext_fn(expr const & e);
-inline expr mk_allext_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_allext_fn(), e1, e2, e3, e4}); }
-expr mk_eps_fn();
-bool is_eps_fn(expr const & e);
-inline bool is_eps(expr const & e) { return is_app(e) && is_eps_fn(arg(e, 0)) && num_args(e) == 4; }
-inline expr mk_eps(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_eps_fn(), e1, e2, e3}); }
-expr mk_eps_ax_fn();
-bool is_eps_ax_fn(expr const & e);
-inline expr mk_eps_ax_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_eps_ax_fn(), e1, e2, e3, e4, e5}); }
-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_substp_fn();
-bool is_substp_fn(expr const & e);
-inline expr mk_substp_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_substp_fn(), e1, e2, e3, e4, e5, e6}); }
-expr mk_eps_th_fn();
-bool is_eps_th_fn(expr const & e);
-inline expr mk_eps_th_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_eps_th_fn(), e1, e2, e3, e4}); }
-expr mk_eps_singleton_fn();
-bool is_eps_singleton_fn(expr const & e);
-inline expr mk_eps_singleton_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_eps_singleton_fn(), e1, e2, e3}); }
-expr mk_nonempty_fun_fn();
-bool is_nonempty_fun_fn(expr const & e);
-inline expr mk_nonempty_fun_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_nonempty_fun_fn(), e1, e2, e3}); }
-expr mk_ite_fn();
-bool is_ite_fn(expr const & e);
-inline bool is_ite(expr const & e) { return is_app(e) && is_ite_fn(arg(e, 0)) && num_args(e) == 5; }
-inline expr mk_ite(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_ite_fn(), e1, e2, e3, e4}); }
-expr mk_not_intro_fn();
-bool is_not_intro_fn(expr const & e);
-inline expr mk_not_intro_th(expr const & e1, expr const & e2) { return mk_app({mk_not_intro_fn(), e1, e2}); }
-expr mk_eta_fn();
-bool is_eta_fn(expr const & e);
-inline expr mk_eta_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_eta_fn(), e1, e2, e3}); }
-expr mk_trivial();
-bool is_trivial(expr const & e);
-expr mk_absurd_fn();
-bool is_absurd_fn(expr const & e);
-inline expr mk_absurd_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_absurd_fn(), e1, e2, e3}); }
-expr mk_eqmp_fn();
-bool is_eqmp_fn(expr const & e);
-inline expr mk_eqmp_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_eqmp_fn(), e1, e2, e3, e4}); }
-expr mk_boolcomplete_fn();
-bool is_boolcomplete_fn(expr const & e);
-inline expr mk_boolcomplete_th(expr const & e1) { return mk_app({mk_boolcomplete_fn(), e1}); }
 expr mk_false_elim_fn();
 bool is_false_elim_fn(expr const & e);
 inline expr mk_false_elim_th(expr const & e1, expr const & e2) { return mk_app({mk_false_elim_fn(), e1, e2}); }
-expr mk_imp_trans_fn();
-bool is_imp_trans_fn(expr const & e);
-inline expr mk_imp_trans_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_imp_trans_fn(), e1, e2, e3, e4, e5, e6}); }
-expr mk_imp_eq_trans_fn();
-bool is_imp_eq_trans_fn(expr const & e);
-inline expr mk_imp_eq_trans_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_imp_eq_trans_fn(), e1, e2, e3, e4, e5, e6}); }
-expr mk_eq_imp_trans_fn();
-bool is_eq_imp_trans_fn(expr const & e);
-inline expr mk_eq_imp_trans_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_eq_imp_trans_fn(), e1, e2, e3, e4, e5, e6}); }
-expr mk_not_not_eq_fn();
-bool is_not_not_eq_fn(expr const & e);
-inline expr mk_not_not_eq_th(expr const & e1) { return mk_app({mk_not_not_eq_fn(), e1}); }
-expr mk_not_not_elim_fn();
-bool is_not_not_elim_fn(expr const & e);
-inline expr mk_not_not_elim_th(expr const & e1, expr const & e2) { return mk_app({mk_not_not_elim_fn(), e1, e2}); }
 expr mk_mt_fn();
 bool is_mt_fn(expr const & e);
 inline expr mk_mt_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_mt_fn(), e1, e2, e3, e4}); }
@@ -132,45 +87,76 @@ inline expr mk_contrapos_th(expr const & e1, expr const & e2, expr const & e3, e
 expr mk_absurd_elim_fn();
 bool is_absurd_elim_fn(expr const & e);
 inline expr mk_absurd_elim_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_absurd_elim_fn(), e1, e2, e3, e4}); }
-expr mk_not_imp_eliml_fn();
-bool is_not_imp_eliml_fn(expr const & e);
-inline expr mk_not_imp_eliml_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_not_imp_eliml_fn(), e1, e2, e3}); }
-expr mk_not_imp_elimr_fn();
-bool is_not_imp_elimr_fn(expr const & e);
-inline expr mk_not_imp_elimr_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_not_imp_elimr_fn(), e1, e2, e3}); }
-expr mk_resolve1_fn();
-bool is_resolve1_fn(expr const & e);
-inline expr mk_resolve1_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_resolve1_fn(), e1, e2, e3, e4}); }
-expr mk_and_intro_fn();
-bool is_and_intro_fn(expr const & e);
-inline expr mk_and_intro_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_and_intro_fn(), e1, e2, e3, e4}); }
-expr mk_and_eliml_fn();
-bool is_and_eliml_fn(expr const & e);
-inline expr mk_and_eliml_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_and_eliml_fn(), e1, e2, e3}); }
-expr mk_and_elimr_fn();
-bool is_and_elimr_fn(expr const & e);
-inline expr mk_and_elimr_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_and_elimr_fn(), e1, e2, e3}); }
 expr mk_or_introl_fn();
 bool is_or_introl_fn(expr const & e);
 inline expr mk_or_introl_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_or_introl_fn(), e1, e2, e3}); }
 expr mk_or_intror_fn();
 bool is_or_intror_fn(expr const & e);
 inline expr mk_or_intror_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_or_intror_fn(), e1, e2, e3}); }
-expr mk_or_elim_fn();
-bool is_or_elim_fn(expr const & e);
-inline expr mk_or_elim_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_or_elim_fn(), e1, e2, e3, e4, e5, e6}); }
-expr mk_refute_fn();
-bool is_refute_fn(expr const & e);
-inline expr mk_refute_th(expr const & e1, expr const & e2) { return mk_app({mk_refute_fn(), e1, e2}); }
+expr mk_boolcomplete_fn();
+bool is_boolcomplete_fn(expr const & e);
+inline expr mk_boolcomplete_th(expr const & e1) { return mk_app({mk_boolcomplete_fn(), e1}); }
+expr mk_boolcomplete_swapped_fn();
+bool is_boolcomplete_swapped_fn(expr const & e);
+inline expr mk_boolcomplete_swapped_th(expr const & e1) { return mk_app({mk_boolcomplete_swapped_fn(), e1}); }
+expr mk_resolve1_fn();
+bool is_resolve1_fn(expr const & e);
+inline expr mk_resolve1_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_resolve1_fn(), e1, e2, e3, e4}); }
+expr mk_subst_fn();
+bool is_subst_fn(expr const & e);
+inline expr mk_subst_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_subst_fn(), e1, e2, e3, e4, e5, e6}); }
+expr mk_substp_fn();
+bool is_substp_fn(expr const & e);
+inline expr mk_substp_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_substp_fn(), e1, e2, e3, e4, e5, e6}); }
 expr mk_symm_fn();
 bool is_symm_fn(expr const & e);
 inline expr mk_symm_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_symm_fn(), e1, e2, e3, e4}); }
-expr mk_eqmpr_fn();
-bool is_eqmpr_fn(expr const & e);
-inline expr mk_eqmpr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_eqmpr_fn(), e1, e2, e3, e4}); }
 expr mk_trans_fn();
 bool is_trans_fn(expr const & e);
 inline expr mk_trans_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_trans_fn(), e1, e2, e3, e4, e5, e6}); }
+expr mk_congr1_fn();
+bool is_congr1_fn(expr const & e);
+inline expr mk_congr1_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_congr1_fn(), e1, e2, e3, e4, e5, e6}); }
+expr mk_congr2_fn();
+bool is_congr2_fn(expr const & e);
+inline expr mk_congr2_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_congr2_fn(), e1, e2, e3, e4, e5, e6}); }
+expr mk_congr_fn();
+bool is_congr_fn(expr const & e);
+inline expr mk_congr_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_congr_fn(), e1, e2, e3, e4, e5, e6, e7, e8}); }
+expr mk_true_ne_false();
+bool is_true_ne_false(expr const & e);
+expr mk_absurd_not_true_fn();
+bool is_absurd_not_true_fn(expr const & e);
+inline expr mk_absurd_not_true_th(expr const & e1) { return mk_app({mk_absurd_not_true_fn(), e1}); }
+expr mk_not_false_trivial();
+bool is_not_false_trivial(expr const & e);
+expr mk_eqmp_fn();
+bool is_eqmp_fn(expr const & e);
+inline expr mk_eqmp_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_eqmp_fn(), e1, e2, e3, e4}); }
+expr mk_eqmpr_fn();
+bool is_eqmpr_fn(expr const & e);
+inline expr mk_eqmpr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_eqmpr_fn(), e1, e2, e3, e4}); }
+expr mk_imp_trans_fn();
+bool is_imp_trans_fn(expr const & e);
+inline expr mk_imp_trans_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_imp_trans_fn(), e1, e2, e3, e4, e5, e6}); }
+expr mk_imp_eq_trans_fn();
+bool is_imp_eq_trans_fn(expr const & e);
+inline expr mk_imp_eq_trans_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_imp_eq_trans_fn(), e1, e2, e3, e4, e5, e6}); }
+expr mk_eq_imp_trans_fn();
+bool is_eq_imp_trans_fn(expr const & e);
+inline expr mk_eq_imp_trans_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_eq_imp_trans_fn(), e1, e2, e3, e4, e5, e6}); }
+expr mk_to_eq_fn();
+bool is_to_eq_fn(expr const & e);
+inline expr mk_to_eq_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_to_eq_fn(), e1, e2, e3, e4}); }
+expr mk_to_heq_fn();
+bool is_to_heq_fn(expr const & e);
+inline expr mk_to_heq_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_to_heq_fn(), e1, e2, e3, e4}); }
+expr mk_iff_eliml_fn();
+bool is_iff_eliml_fn(expr const & e);
+inline expr mk_iff_eliml_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_iff_eliml_fn(), e1, e2, e3, e4}); }
+expr mk_iff_elimr_fn();
+bool is_iff_elimr_fn(expr const & e);
+inline expr mk_iff_elimr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_iff_elimr_fn(), e1, e2, e3, e4}); }
 expr mk_ne_symm_fn();
 bool is_ne_symm_fn(expr const & e);
 inline expr mk_ne_symm_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_ne_symm_fn(), e1, e2, e3, e4}); }
@@ -186,63 +172,73 @@ inline expr mk_eqt_elim_th(expr const & e1, expr const & e2) { return mk_app({mk
 expr mk_eqf_elim_fn();
 bool is_eqf_elim_fn(expr const & e);
 inline expr mk_eqf_elim_th(expr const & e1, expr const & e2) { return mk_app({mk_eqf_elim_fn(), e1, e2}); }
-expr mk_congr1_fn();
-bool is_congr1_fn(expr const & e);
-inline expr mk_congr1_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_congr1_fn(), e1, e2, e3, e4, e5, e6}); }
-expr mk_congr2_fn();
-bool is_congr2_fn(expr const & e);
-inline expr mk_congr2_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_congr2_fn(), e1, e2, e3, e4, e5, e6}); }
-expr mk_congr_fn();
-bool is_congr_fn(expr const & e);
-inline expr mk_congr_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_congr_fn(), e1, e2, e3, e4, e5, e6, e7, e8}); }
-expr mk_exists_elim_fn();
-bool is_exists_elim_fn(expr const & e);
-inline expr mk_exists_elim_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_exists_elim_fn(), e1, e2, e3, e4, e5}); }
-expr mk_exists_intro_fn();
-bool is_exists_intro_fn(expr const & e);
-inline expr mk_exists_intro_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_exists_intro_fn(), e1, e2, e3, e4}); }
-expr mk_nonempty_elim_fn();
-bool is_nonempty_elim_fn(expr const & e);
-inline expr mk_nonempty_elim_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_nonempty_elim_fn(), e1, e2, e3, e4}); }
-expr mk_nonempty_ex_intro_fn();
-bool is_nonempty_ex_intro_fn(expr const & e);
-inline expr mk_nonempty_ex_intro_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_nonempty_ex_intro_fn(), e1, e2, e3}); }
-expr mk_exists_to_eps_fn();
-bool is_exists_to_eps_fn(expr const & e);
-inline expr mk_exists_to_eps_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_exists_to_eps_fn(), e1, e2, e3}); }
-expr mk_axiom_of_choice_fn();
-bool is_axiom_of_choice_fn(expr const & e);
-inline expr mk_axiom_of_choice_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_axiom_of_choice_fn(), e1, e2, e3, e4}); }
+expr mk_heqt_elim_fn();
+bool is_heqt_elim_fn(expr const & e);
+inline expr mk_heqt_elim_th(expr const & e1, expr const & e2) { return mk_app({mk_heqt_elim_fn(), e1, e2}); }
+expr mk_not_true();
+bool is_not_true(expr const & e);
+expr mk_not_false();
+bool is_not_false(expr const & e);
+expr mk_not_not_eq_fn();
+bool is_not_not_eq_fn(expr const & e);
+inline expr mk_not_not_eq_th(expr const & e1) { return mk_app({mk_not_not_eq_fn(), e1}); }
+expr mk_not_neq_fn();
+bool is_not_neq_fn(expr const & e);
+inline expr mk_not_neq_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_not_neq_fn(), e1, e2, e3}); }
+expr mk_not_neq_elim_fn();
+bool is_not_neq_elim_fn(expr const & e);
+inline expr mk_not_neq_elim_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_not_neq_elim_fn(), e1, e2, e3, e4}); }
+expr mk_not_not_elim_fn();
+bool is_not_not_elim_fn(expr const & e);
+inline expr mk_not_not_elim_th(expr const & e1, expr const & e2) { return mk_app({mk_not_not_elim_fn(), e1, e2}); }
+expr mk_not_imp_eliml_fn();
+bool is_not_imp_eliml_fn(expr const & e);
+inline expr mk_not_imp_eliml_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_not_imp_eliml_fn(), e1, e2, e3}); }
+expr mk_not_imp_elimr_fn();
+bool is_not_imp_elimr_fn(expr const & e);
+inline expr mk_not_imp_elimr_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_not_imp_elimr_fn(), e1, e2, e3}); }
+expr mk_and_intro_fn();
+bool is_and_intro_fn(expr const & e);
+inline expr mk_and_intro_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_and_intro_fn(), e1, e2, e3, e4}); }
+expr mk_and_eliml_fn();
+bool is_and_eliml_fn(expr const & e);
+inline expr mk_and_eliml_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_and_eliml_fn(), e1, e2, e3}); }
+expr mk_and_elimr_fn();
+bool is_and_elimr_fn(expr const & e);
+inline expr mk_and_elimr_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_and_elimr_fn(), e1, e2, e3}); }
+expr mk_or_elim_fn();
+bool is_or_elim_fn(expr const & e);
+inline expr mk_or_elim_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_or_elim_fn(), e1, e2, e3, e4, e5, e6}); }
+expr mk_refute_fn();
+bool is_refute_fn(expr const & e);
+inline expr mk_refute_th(expr const & e1, expr const & e2) { return mk_app({mk_refute_fn(), e1, e2}); }
 expr mk_boolext_fn();
 bool is_boolext_fn(expr const & e);
 inline expr mk_boolext_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_boolext_fn(), e1, e2, e3, e4}); }
 expr mk_iff_intro_fn();
 bool is_iff_intro_fn(expr const & e);
 inline expr mk_iff_intro_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_iff_intro_fn(), e1, e2, e3, e4}); }
-expr mk_iff_eliml_fn();
-bool is_iff_eliml_fn(expr const & e);
-inline expr mk_iff_eliml_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_iff_eliml_fn(), e1, e2, e3, e4}); }
-expr mk_iff_elimr_fn();
-bool is_iff_elimr_fn(expr const & e);
-inline expr mk_iff_elimr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_iff_elimr_fn(), e1, e2, e3, e4}); }
-expr mk_skolem_th_fn();
-bool is_skolem_th_fn(expr const & e);
-inline expr mk_skolem_th_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_skolem_th_fn(), e1, e2, e3}); }
 expr mk_eqt_intro_fn();
 bool is_eqt_intro_fn(expr const & e);
 inline expr mk_eqt_intro_th(expr const & e1, expr const & e2) { return mk_app({mk_eqt_intro_fn(), e1, e2}); }
 expr mk_eqf_intro_fn();
 bool is_eqf_intro_fn(expr const & e);
 inline expr mk_eqf_intro_th(expr const & e1, expr const & e2) { return mk_app({mk_eqf_intro_fn(), e1, e2}); }
-expr mk_neq_elim_fn();
-bool is_neq_elim_fn(expr const & e);
-inline expr mk_neq_elim_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_neq_elim_fn(), e1, e2, e3, e4}); }
+expr mk_a_neq_a_fn();
+bool is_a_neq_a_fn(expr const & e);
+inline expr mk_a_neq_a_th(expr const & e1, expr const & e2) { return mk_app({mk_a_neq_a_fn(), e1, e2}); }
 expr mk_eq_id_fn();
 bool is_eq_id_fn(expr const & e);
 inline expr mk_eq_id_th(expr const & e1, expr const & e2) { return mk_app({mk_eq_id_fn(), e1, e2}); }
 expr mk_iff_id_fn();
 bool is_iff_id_fn(expr const & e);
 inline expr mk_iff_id_th(expr const & e1) { return mk_app({mk_iff_id_fn(), e1}); }
+expr mk_neq_elim_fn();
+bool is_neq_elim_fn(expr const & e);
+inline expr mk_neq_elim_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_neq_elim_fn(), e1, e2, e3, e4}); }
+expr mk_neq_to_not_eq_fn();
+bool is_neq_to_not_eq_fn(expr const & e);
+inline expr mk_neq_to_not_eq_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_neq_to_not_eq_fn(), e1, e2, e3}); }
 expr mk_left_comm_fn();
 bool is_left_comm_fn(expr const & e);
 inline expr mk_left_comm_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_left_comm_fn(), e1, e2, e3, e4, e5, e6, e7}); }
@@ -273,6 +269,9 @@ inline expr mk_or_tauto_th(expr const & e1) { return mk_app({mk_or_tauto_fn(), e
 expr mk_or_left_comm_fn();
 bool is_or_left_comm_fn(expr const & e);
 inline expr mk_or_left_comm_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_or_left_comm_fn(), e1, e2, e3}); }
+expr mk_resolve2_fn();
+bool is_resolve2_fn(expr const & e);
+inline expr mk_resolve2_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_resolve2_fn(), e1, e2, e3, e4}); }
 expr mk_and_comm_fn();
 bool is_and_comm_fn(expr const & e);
 inline expr mk_and_comm_th(expr const & e1, expr const & e2) { return mk_app({mk_and_comm_fn(), e1, e2}); }
@@ -318,58 +317,15 @@ inline expr mk_imp_id_th(expr const & e1) { return mk_app({mk_imp_id_fn(), e1});
 expr mk_imp_or_fn();
 bool is_imp_or_fn(expr const & e);
 inline expr mk_imp_or_th(expr const & e1, expr const & e2) { return mk_app({mk_imp_or_fn(), e1, e2}); }
-expr mk_not_true();
-bool is_not_true(expr const & e);
-expr mk_not_false();
-bool is_not_false(expr const & e);
-expr mk_not_neq_fn();
-bool is_not_neq_fn(expr const & e);
-inline expr mk_not_neq_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_not_neq_fn(), e1, e2, e3}); }
-expr mk_not_neq_elim_fn();
-bool is_not_neq_elim_fn(expr const & e);
-inline expr mk_not_neq_elim_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_not_neq_elim_fn(), e1, e2, e3, e4}); }
-expr mk_not_and_fn();
-bool is_not_and_fn(expr const & e);
-inline expr mk_not_and_th(expr const & e1, expr const & e2) { return mk_app({mk_not_and_fn(), e1, e2}); }
-expr mk_not_and_elim_fn();
-bool is_not_and_elim_fn(expr const & e);
-inline expr mk_not_and_elim_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_not_and_elim_fn(), e1, e2, e3}); }
-expr mk_not_or_fn();
-bool is_not_or_fn(expr const & e);
-inline expr mk_not_or_th(expr const & e1, expr const & e2) { return mk_app({mk_not_or_fn(), e1, e2}); }
-expr mk_not_or_elim_fn();
-bool is_not_or_elim_fn(expr const & e);
-inline expr mk_not_or_elim_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_not_or_elim_fn(), e1, e2, e3}); }
-expr mk_not_iff_fn();
-bool is_not_iff_fn(expr const & e);
-inline expr mk_not_iff_th(expr const & e1, expr const & e2) { return mk_app({mk_not_iff_fn(), e1, e2}); }
-expr mk_not_iff_elim_fn();
-bool is_not_iff_elim_fn(expr const & e);
-inline expr mk_not_iff_elim_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_not_iff_elim_fn(), e1, e2, e3}); }
-expr mk_not_implies_fn();
-bool is_not_implies_fn(expr const & e);
-inline expr mk_not_implies_th(expr const & e1, expr const & e2) { return mk_app({mk_not_implies_fn(), e1, e2}); }
-expr mk_not_implies_elim_fn();
-bool is_not_implies_elim_fn(expr const & e);
-inline expr mk_not_implies_elim_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_not_implies_elim_fn(), e1, e2, e3}); }
 expr mk_not_congr_fn();
 bool is_not_congr_fn(expr const & e);
 inline expr mk_not_congr_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_not_congr_fn(), e1, e2, e3}); }
-expr mk_exists_rem_fn();
-bool is_exists_rem_fn(expr const & e);
-inline expr mk_exists_rem_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_exists_rem_fn(), e1, e2, e3}); }
-expr mk_forall_rem_fn();
-bool is_forall_rem_fn(expr const & e);
-inline expr mk_forall_rem_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_forall_rem_fn(), e1, e2, e3}); }
-expr mk_eq_exists_intro_fn();
-bool is_eq_exists_intro_fn(expr const & e);
-inline expr mk_eq_exists_intro_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_eq_exists_intro_fn(), e1, e2, e3, e4}); }
-expr mk_not_forall_fn();
-bool is_not_forall_fn(expr const & e);
-inline expr mk_not_forall_th(expr const & e1, expr const & e2) { return mk_app({mk_not_forall_fn(), e1, e2}); }
-expr mk_not_forall_elim_fn();
-bool is_not_forall_elim_fn(expr const & e);
-inline expr mk_not_forall_elim_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_not_forall_elim_fn(), e1, e2, e3}); }
+expr mk_exists_elim_fn();
+bool is_exists_elim_fn(expr const & e);
+inline expr mk_exists_elim_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_exists_elim_fn(), e1, e2, e3, e4, e5}); }
+expr mk_exists_intro_fn();
+bool is_exists_intro_fn(expr const & e);
+inline expr mk_exists_intro_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_exists_intro_fn(), e1, e2, e3, e4}); }
 expr mk_not_exists_fn();
 bool is_not_exists_fn(expr const & e);
 inline expr mk_not_exists_th(expr const & e1, expr const & e2) { return mk_app({mk_not_exists_fn(), e1, e2}); }
@@ -385,6 +341,28 @@ inline expr mk_exists_unfold2_th(expr const & e1, expr const & e2, expr const &
 expr mk_exists_unfold_fn();
 bool is_exists_unfold_fn(expr const & e);
 inline expr mk_exists_unfold_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_exists_unfold_fn(), e1, e2, e3}); }
+expr mk_inhabited_fn();
+bool is_inhabited_fn(expr const & e);
+inline bool is_inhabited(expr const & e) { return is_app(e) && is_inhabited_fn(arg(e, 0)) && num_args(e) == 2; }
+inline expr mk_inhabited(expr const & e1) { return mk_app({mk_inhabited_fn(), e1}); }
+expr mk_inhabited_intro_fn();
+bool is_inhabited_intro_fn(expr const & e);
+inline expr mk_inhabited_intro_th(expr const & e1, expr const & e2) { return mk_app({mk_inhabited_intro_fn(), e1, e2}); }
+expr mk_inhabited_elim_fn();
+bool is_inhabited_elim_fn(expr const & e);
+inline expr mk_inhabited_elim_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_inhabited_elim_fn(), e1, e2, e3, e4}); }
+expr mk_inhabited_ex_intro_fn();
+bool is_inhabited_ex_intro_fn(expr const & e);
+inline expr mk_inhabited_ex_intro_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_inhabited_ex_intro_fn(), e1, e2, e3}); }
+expr mk_inhabited_range_fn();
+bool is_inhabited_range_fn(expr const & e);
+inline expr mk_inhabited_range_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_inhabited_range_fn(), e1, e2, e3, e4}); }
+expr mk_exists_rem_fn();
+bool is_exists_rem_fn(expr const & e);
+inline expr mk_exists_rem_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_exists_rem_fn(), e1, e2, e3}); }
+expr mk_forall_rem_fn();
+bool is_forall_rem_fn(expr const & e);
+inline expr mk_forall_rem_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_forall_rem_fn(), e1, e2, e3}); }
 expr mk_imp_congrr_fn();
 bool is_imp_congrr_fn(expr const & e);
 inline expr mk_imp_congrr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_imp_congrr_fn(), e1, e2, e3, e4, e5, e6}); }
@@ -412,6 +390,50 @@ inline expr mk_and_congrl_th(expr const & e1, expr const & e2, expr const & e3,
 expr mk_and_congr_fn();
 bool is_and_congr_fn(expr const & e);
 inline expr mk_and_congr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_and_congr_fn(), e1, e2, e3, e4, e5, e6}); }
+expr mk_not_and_fn();
+bool is_not_and_fn(expr const & e);
+inline expr mk_not_and_th(expr const & e1, expr const & e2) { return mk_app({mk_not_and_fn(), e1, e2}); }
+expr mk_not_and_elim_fn();
+bool is_not_and_elim_fn(expr const & e);
+inline expr mk_not_and_elim_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_not_and_elim_fn(), e1, e2, e3}); }
+expr mk_not_or_fn();
+bool is_not_or_fn(expr const & e);
+inline expr mk_not_or_th(expr const & e1, expr const & e2) { return mk_app({mk_not_or_fn(), e1, e2}); }
+expr mk_not_or_elim_fn();
+bool is_not_or_elim_fn(expr const & e);
+inline expr mk_not_or_elim_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_not_or_elim_fn(), e1, e2, e3}); }
+expr mk_not_implies_fn();
+bool is_not_implies_fn(expr const & e);
+inline expr mk_not_implies_th(expr const & e1, expr const & e2) { return mk_app({mk_not_implies_fn(), e1, e2}); }
+expr mk_not_implies_elim_fn();
+bool is_not_implies_elim_fn(expr const & e);
+inline expr mk_not_implies_elim_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_not_implies_elim_fn(), e1, e2, e3}); }
+expr mk_a_eq_not_a_fn();
+bool is_a_eq_not_a_fn(expr const & e);
+inline expr mk_a_eq_not_a_th(expr const & e1) { return mk_app({mk_a_eq_not_a_fn(), e1}); }
+expr mk_a_iff_not_a_fn();
+bool is_a_iff_not_a_fn(expr const & e);
+inline expr mk_a_iff_not_a_th(expr const & e1) { return mk_app({mk_a_iff_not_a_fn(), e1}); }
+expr mk_true_eq_false();
+bool is_true_eq_false(expr const & e);
+expr mk_true_iff_false();
+bool is_true_iff_false(expr const & e);
+expr mk_false_eq_true();
+bool is_false_eq_true(expr const & e);
+expr mk_false_iff_true();
+bool is_false_iff_true(expr const & e);
+expr mk_a_iff_true_fn();
+bool is_a_iff_true_fn(expr const & e);
+inline expr mk_a_iff_true_th(expr const & e1) { return mk_app({mk_a_iff_true_fn(), e1}); }
+expr mk_a_iff_false_fn();
+bool is_a_iff_false_fn(expr const & e);
+inline expr mk_a_iff_false_th(expr const & e1) { return mk_app({mk_a_iff_false_fn(), e1}); }
+expr mk_not_iff_fn();
+bool is_not_iff_fn(expr const & e);
+inline expr mk_not_iff_th(expr const & e1, expr const & e2) { return mk_app({mk_not_iff_fn(), e1, e2}); }
+expr mk_not_iff_elim_fn();
+bool is_not_iff_elim_fn(expr const & e);
+inline expr mk_not_iff_elim_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_not_iff_elim_fn(), e1, e2, e3}); }
 expr mk_forall_or_distributer_fn();
 bool is_forall_or_distributer_fn(expr const & e);
 inline expr mk_forall_or_distributer_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_forall_or_distributer_fn(), e1, e2, e3}); }
@@ -424,18 +446,65 @@ inline expr mk_forall_and_distribute_th(expr const & e1, expr const & e2, expr c
 expr mk_exists_and_distributer_fn();
 bool is_exists_and_distributer_fn(expr const & e);
 inline expr mk_exists_and_distributer_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_exists_and_distributer_fn(), e1, e2, e3}); }
-expr mk_exists_and_distributel_fn();
-bool is_exists_and_distributel_fn(expr const & e);
-inline expr mk_exists_and_distributel_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_exists_and_distributel_fn(), e1, e2, e3}); }
 expr mk_exists_or_distribute_fn();
 bool is_exists_or_distribute_fn(expr const & e);
 inline expr mk_exists_or_distribute_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_exists_or_distribute_fn(), e1, e2, e3}); }
+expr mk_eq_exists_intro_fn();
+bool is_eq_exists_intro_fn(expr const & e);
+inline expr mk_eq_exists_intro_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_eq_exists_intro_fn(), e1, e2, e3, e4}); }
+expr mk_not_forall_fn();
+bool is_not_forall_fn(expr const & e);
+inline expr mk_not_forall_th(expr const & e1, expr const & e2) { return mk_app({mk_not_forall_fn(), e1, e2}); }
+expr mk_not_forall_elim_fn();
+bool is_not_forall_elim_fn(expr const & e);
+inline expr mk_not_forall_elim_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_not_forall_elim_fn(), e1, e2, e3}); }
+expr mk_exists_and_distributel_fn();
+bool is_exists_and_distributel_fn(expr const & e);
+inline expr mk_exists_and_distributel_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_exists_and_distributel_fn(), e1, e2, e3}); }
 expr mk_exists_imp_distribute_fn();
 bool is_exists_imp_distribute_fn(expr const & e);
 inline expr mk_exists_imp_distribute_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_exists_imp_distribute_fn(), e1, e2, e3}); }
-expr mk_nonempty_range_fn();
-bool is_nonempty_range_fn(expr const & e);
-inline expr mk_nonempty_range_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_nonempty_range_fn(), e1, e2, e3, e4}); }
+expr mk_forall_uninhabited_fn();
+bool is_forall_uninhabited_fn(expr const & e);
+inline expr mk_forall_uninhabited_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_forall_uninhabited_fn(), e1, e2, e3, e4}); }
+expr mk_allext_fn();
+bool is_allext_fn(expr const & e);
+inline expr mk_allext_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_allext_fn(), e1, e2, e3, e4}); }
+expr mk_funext_fn();
+bool is_funext_fn(expr const & e);
+inline expr mk_funext_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_funext_fn(), e1, e2, e3, e4, e5}); }
+expr mk_eta_fn();
+bool is_eta_fn(expr const & e);
+inline expr mk_eta_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_eta_fn(), e1, e2, e3}); }
+expr mk_eps_fn();
+bool is_eps_fn(expr const & e);
+inline bool is_eps(expr const & e) { return is_app(e) && is_eps_fn(arg(e, 0)) && num_args(e) == 4; }
+inline expr mk_eps(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_eps_fn(), e1, e2, e3}); }
+expr mk_eps_ax_fn();
+bool is_eps_ax_fn(expr const & e);
+inline expr mk_eps_ax_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_eps_ax_fn(), e1, e2, e3, e4, e5}); }
+expr mk_eps_th_fn();
+bool is_eps_th_fn(expr const & e);
+inline expr mk_eps_th_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_eps_th_fn(), e1, e2, e3, e4}); }
+expr mk_eps_singleton_fn();
+bool is_eps_singleton_fn(expr const & e);
+inline expr mk_eps_singleton_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_eps_singleton_fn(), e1, e2, e3}); }
+expr mk_inhabited_fun_fn();
+bool is_inhabited_fun_fn(expr const & e);
+inline expr mk_inhabited_fun_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_inhabited_fun_fn(), e1, e2, e3}); }
+expr mk_exists_to_eps_fn();
+bool is_exists_to_eps_fn(expr const & e);
+inline expr mk_exists_to_eps_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_exists_to_eps_fn(), e1, e2, e3}); }
+expr mk_axiom_of_choice_fn();
+bool is_axiom_of_choice_fn(expr const & e);
+inline expr mk_axiom_of_choice_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_axiom_of_choice_fn(), e1, e2, e3, e4}); }
+expr mk_skolem_th_fn();
+bool is_skolem_th_fn(expr const & e);
+inline expr mk_skolem_th_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_skolem_th_fn(), e1, e2, e3}); }
+expr mk_ite_fn();
+bool is_ite_fn(expr const & e);
+inline bool is_ite(expr const & e) { return is_app(e) && is_ite_fn(arg(e, 0)) && num_args(e) == 5; }
+inline expr mk_ite(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_ite_fn(), e1, e2, e3, e4}); }
 expr mk_if_true_fn();
 bool is_if_true_fn(expr const & e);
 inline expr mk_if_true_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_if_true_fn(), e1, e2, e3}); }
@@ -463,4 +532,19 @@ inline expr mk_eq_if_distributer_th(expr const & e1, expr const & e2, expr const
 expr mk_eq_if_distributel_fn();
 bool is_eq_if_distributel_fn(expr const & e);
 inline expr mk_eq_if_distributel_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_eq_if_distributel_fn(), e1, e2, e3, e4, e5}); }
+expr mk_injective_fn();
+bool is_injective_fn(expr const & e);
+inline bool is_injective(expr const & e) { return is_app(e) && is_injective_fn(arg(e, 0)) && num_args(e) == 4; }
+inline expr mk_injective(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_injective_fn(), e1, e2, e3}); }
+expr mk_non_surjective_fn();
+bool is_non_surjective_fn(expr const & e);
+inline bool is_non_surjective(expr const & e) { return is_app(e) && is_non_surjective_fn(arg(e, 0)) && num_args(e) == 4; }
+inline expr mk_non_surjective(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_non_surjective_fn(), e1, e2, e3}); }
+expr mk_ind();
+bool is_ind(expr const & e);
+expr mk_infinity();
+bool is_infinity(expr const & e);
+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}); }
 }
diff --git a/src/kernel/normalizer.cpp b/src/kernel/normalizer.cpp
index 965553755..c41c2010f 100644
--- a/src/kernel/normalizer.cpp
+++ b/src/kernel/normalizer.cpp
@@ -232,21 +232,9 @@ class normalizer::imp {
 
         expr r;
         switch (a.kind()) {
-        case expr_kind::Pi: {
-            if (is_arrow(a)) {
-                expr new_d = reify(normalize(abst_domain(a), s, k), k);
-                if (is_bool_value(new_d)) {
-                    m_cache.clear();
-                    expr new_b = reify(normalize(abst_body(a), extend(s, mk_var(k)), k+1), k+1);
-                    if (is_bool_value(new_b)) {
-                        r = mk_bool_value(is_false(new_d) || is_true(new_b));
-                        break;
-                    }
-                }
-            }
+        case expr_kind::Pi:
             r = mk_closure(a, m_ctx, s);
             break;
-        }
         case expr_kind::MetaVar: case expr_kind::Lambda:
             r = mk_closure(a, m_ctx, s);
             break;
diff --git a/src/library/cast_decls.cpp b/src/library/cast_decls.cpp
index 57b52a09f..13acd55d3 100644
--- a/src/library/cast_decls.cpp
+++ b/src/library/cast_decls.cpp
@@ -6,10 +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(cast_fn, name("cast"));
-MK_CONSTANT(cast_heq_fn, name("cast_heq"));
-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/cast_decls.h b/src/library/cast_decls.h
index c492859d5..2776d59c2 100644
--- a/src/library/cast_decls.h
+++ b/src/library/cast_decls.h
@@ -5,23 +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_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_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/src/library/heq_decls.cpp b/src/library/heq_decls.cpp
index d96b03b86..70ccf29d6 100644
--- a/src/library/heq_decls.cpp
+++ b/src/library/heq_decls.cpp
@@ -6,17 +6,17 @@ 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(heq_fn, name("heq"));
-MK_CONSTANT(heq_eq_fn, name("heq_eq"));
-MK_CONSTANT(to_eq_fn, name("to_eq"));
-MK_CONSTANT(to_heq_fn, name("to_heq"));
-MK_CONSTANT(hrefl_fn, name("hrefl"));
-MK_CONSTANT(heqt_elim_fn, name("heqt_elim"));
+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(TypeM, name("TypeM"));
 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 32336d3c2..4e89e43d1 100644
--- a/src/library/heq_decls.h
+++ b/src/library/heq_decls.h
@@ -5,25 +5,15 @@ 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_heq_fn();
-bool is_heq_fn(expr const & e);
-inline bool is_heq(expr const & e) { return is_app(e) && is_heq_fn(arg(e, 0)) && num_args(e) == 5; }
-inline expr mk_heq(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_heq_fn(), e1, e2, e3, e4}); }
-expr mk_heq_eq_fn();
-bool is_heq_eq_fn(expr const & e);
-inline expr mk_heq_eq_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_heq_eq_fn(), e1, e2, e3}); }
-expr mk_to_eq_fn();
-bool is_to_eq_fn(expr const & e);
-inline expr mk_to_eq_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_to_eq_fn(), e1, e2, e3, e4}); }
-expr mk_to_heq_fn();
-bool is_to_heq_fn(expr const & e);
-inline expr mk_to_heq_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_to_heq_fn(), e1, e2, e3, e4}); }
-expr mk_hrefl_fn();
-bool is_hrefl_fn(expr const & e);
-inline expr mk_hrefl_th(expr const & e1, expr const & e2) { return mk_app({mk_hrefl_fn(), e1, e2}); }
-expr mk_heqt_elim_fn();
-bool is_heqt_elim_fn(expr const & e);
-inline expr mk_heqt_elim_th(expr const & e1, expr const & e2) { return mk_app({mk_heqt_elim_fn(), e1, e2}); }
+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}); }
@@ -33,8 +23,6 @@ inline expr mk_htrans_th(expr const & e1, expr const & e2, expr const & e3, expr
 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_TypeM();
-bool is_TypeM(expr const & e);
 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}); }
@@ -44,4 +32,16 @@ inline expr mk_hsfunext_th(expr const & e1, expr const & e2, expr const & e3, ex
 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/src/library/simplifier/simplifier.cpp b/src/library/simplifier/simplifier.cpp
index 119400cb7..4bca47168 100644
--- a/src/library/simplifier/simplifier.cpp
+++ b/src/library/simplifier/simplifier.cpp
@@ -209,7 +209,7 @@ class simplifier_cell::imp {
     expr ensure_pi(expr const & e) { return m_tc.ensure_pi(e, context(), m_menv.to_some_menv()); }
     expr normalize(expr const & e) {
         normalizer & proc = m_tc.get_normalizer();
-        return proc(e, context(), m_menv.to_some_menv(), true);
+        return proc(e, context(), m_menv.to_some_menv());
     }
     expr lift_free_vars(expr const & e, unsigned s, unsigned d) { return ::lean::lift_free_vars(e, s, d, m_menv.to_some_menv()); }
     expr lower_free_vars(expr const & e, unsigned s, unsigned d) { return ::lean::lower_free_vars(e, s, d, m_menv.to_some_menv()); }
@@ -760,7 +760,7 @@ class simplifier_cell::imp {
     static bool is_value(expr const & e) {
         // Currently only semantic attachments are treated as value.
         // We may relax that in the future.
-        return ::lean::is_value(e);
+        return ::lean::is_value(e) || is_true(e) || is_false(e);
     }
 
     /**
diff --git a/src/tests/library/arith.cpp b/src/tests/library/arith.cpp
index 979230cc6..f1b2f43fa 100644
--- a/src/tests/library/arith.cpp
+++ b/src/tests/library/arith.cpp
@@ -23,28 +23,12 @@ static void tst0() {
     env->add_var("n", Nat);
     expr n = Const("n");
     lean_assert_eq(mk_nat_type(), Nat);
-    lean_assert_eq(norm(mk_Nat_mul(nVal(2), nVal(3))), nVal(6));
-    lean_assert_eq(norm(mk_Nat_le(nVal(2), nVal(3))), True);
-    lean_assert_eq(norm(mk_Nat_le(nVal(5), nVal(3))), False);
-    lean_assert_eq(norm(mk_Nat_le(nVal(2), nVal(3))), True);
-    lean_assert_eq(norm(mk_Nat_le(n, nVal(3))), mk_Nat_le(n, nVal(3)));
     env->add_var("x", Real);
     expr x = Const("x");
     lean_assert_eq(mk_real_type(), Real);
-    lean_assert_eq(norm(mk_Real_mul(rVal(2), rVal(3))), rVal(6));
-    lean_assert_eq(norm(mk_Real_div(rVal(2), rVal(0))), rVal(0));
-    lean_assert_eq(norm(mk_Real_le(rVal(2),  rVal(3))), True);
-    lean_assert_eq(norm(mk_Real_le(rVal(5),  rVal(3))), False);
-    lean_assert_eq(norm(mk_Real_le(rVal(2),  rVal(3))), True);
-    lean_assert_eq(norm(mk_Real_le(x, rVal(3))), mk_Real_le(x, rVal(3)));
     env->add_var("i", Int);
     expr i = Const("i");
-    lean_assert_eq(norm(mk_int_to_real(i)), mk_int_to_real(i));
-    lean_assert_eq(norm(mk_int_to_real(iVal(2))), rVal(2));
     lean_assert_eq(mk_int_type(), Int);
-    lean_assert_eq(norm(mk_nat_to_int(n)), mk_nat_to_int(n));
-    lean_assert_eq(norm(mk_nat_to_int(nVal(2))), iVal(2));
-    lean_assert_eq(norm(mk_Int_div(iVal(2), iVal(0))), iVal(0));
 }
 
 static void tst1() {
@@ -62,15 +46,12 @@ static void tst2() {
     expr e = mk_Int_add(iVal(10), iVal(30));
     std::cout << e << "\n";
     std::cout << normalize(e, env) << "\n";
-    lean_assert(normalize(e, env) == iVal(40));
     std::cout << type_check(mk_Int_add_fn(), env) << "\n";
     lean_assert(type_check(e, env) == Int);
     lean_assert(type_check(mk_app(mk_Int_add_fn(), iVal(10)), env) == (Int >> Int));
-    lean_assert(is_int_value(normalize(e, env)));
     expr e2 = Fun("a", Int, mk_Int_add(Const("a"), mk_Int_add(iVal(10), iVal(30))));
     std::cout << e2 << " --> " << normalize(e2, env) << "\n";
     lean_assert(type_check(e2, env) == mk_arrow(Int, Int));
-    lean_assert(normalize(e2, env) == Fun("a", Int, mk_Int_add(Const("a"), iVal(40))));
 }
 
 static void tst3() {
@@ -79,15 +60,12 @@ static void tst3() {
     expr e = mk_Int_mul(iVal(10), iVal(30));
     std::cout << e << "\n";
     std::cout << normalize(e, env) << "\n";
-    lean_assert(normalize(e, env) == iVal(300));
     std::cout << type_check(mk_Int_mul_fn(), env) << "\n";
     lean_assert(type_check(e, env) == Int);
     lean_assert(type_check(mk_app(mk_Int_mul_fn(), iVal(10)), env) == mk_arrow(Int, Int));
-    lean_assert(is_int_value(normalize(e, env)));
     expr e2 = Fun("a", Int, mk_Int_mul(Const("a"), mk_Int_mul(iVal(10), iVal(30))));
     std::cout << e2 << " --> " << normalize(e2, env) << "\n";
     lean_assert(type_check(e2, env) == (Int >> Int));
-    lean_assert(normalize(e2, env) == Fun("a", Int, mk_Int_mul(Const("a"), iVal(300))));
 }
 
 static void tst4() {
@@ -96,15 +74,12 @@ static void tst4() {
     expr e = mk_Int_sub(iVal(10), iVal(30));
     std::cout << e << "\n";
     std::cout << normalize(e, env) << "\n";
-    lean_assert(normalize(e, env, context(), true) == iVal(-20));
     std::cout << type_check(mk_Int_sub_fn(), env) << "\n";
     lean_assert(type_check(e, env) == Int);
     lean_assert(type_check(mk_app(mk_Int_sub_fn(), iVal(10)), env) == mk_arrow(Int, Int));
-    lean_assert(is_int_value(normalize(e, env, context(), true)));
     expr e2 = Fun("a", Int, mk_Int_sub(Const("a"), mk_Int_sub(iVal(10), iVal(30))));
     std::cout << e2 << " --> " << normalize(e2, env) << "\n";
     lean_assert(type_check(e2, env) == (Int >> Int));
-    lean_assert_eq(normalize(e2, env, context(), true), Fun("a", Int, mk_Int_add(Const("a"), iVal(20))));
 }
 
 static void tst5() {
@@ -113,8 +88,6 @@ static void tst5() {
     env->add_var(name("a"), Int);
     expr e = mk_eq(Int, iVal(3), iVal(4));
     std::cout << e << " --> " << normalize(e, env) << "\n";
-    lean_assert(normalize(e, env) == False);
-    lean_assert(normalize(mk_eq(Int, Const("a"), iVal(3)), env) == mk_eq(Int, Const("a"), iVal(3)));
 }
 
 static void tst6() {
diff --git a/tests/lean/add_assoc.lean.expected.out b/tests/lean/add_assoc.lean.expected.out
index 01ea01498..2aeead867 100644
--- a/tests/lean/add_assoc.lean.expected.out
+++ b/tests/lean/add_assoc.lean.expected.out
@@ -5,7 +5,7 @@
   Proved: add_assoc
 Nat::add_zerol : ∀ a : ℕ, 0 + a = a
 Nat::add_succl : ∀ a b : ℕ, a + 1 + b = a + b + 1
-@eq_id : ∀ (A : TypeU) (a : A), a = a ↔ ⊤
+@eq_id : ∀ (A : (Type U)) (a : A), a = a ↔ ⊤
 theorem add_assoc (a b c : ℕ) : a + (b + c) = a + b + c :=
     Nat::induction_on
         a
diff --git a/tests/lean/arith1.lean.expected.out b/tests/lean/arith1.lean.expected.out
index d17346ec4..9feb47357 100644
--- a/tests/lean/arith1.lean.expected.out
+++ b/tests/lean/arith1.lean.expected.out
@@ -4,8 +4,8 @@
 10 + 20 : ℕ
 10 : ℕ
 10 - 20 : ℤ
--10
-5
+10 - 20
+25 - 20
 15 + 10 - 20 : ℤ
   Assumed: x
   Assumed: n
diff --git a/tests/lean/arith3.lean.expected.out b/tests/lean/arith3.lean.expected.out
index b62ac1b23..0368671eb 100644
--- a/tests/lean/arith3.lean.expected.out
+++ b/tests/lean/arith3.lean.expected.out
@@ -1,12 +1,12 @@
   Set: pp::colors
   Set: pp::unicode
   Imported 'Int'
+8 mod 3
 2
 2
-2
-1
+7 mod 3
 -8 mod 3
   Set: lean::pp::notation
 Int::mod -8 3
--2
--8
+Int::mod -8 3
+Int::add -6 (Int::mod -8 3)
diff --git a/tests/lean/arith6.lean.expected.out b/tests/lean/arith6.lean.expected.out
index d61b0bc2f..c2180f2f0 100644
--- a/tests/lean/arith6.lean.expected.out
+++ b/tests/lean/arith6.lean.expected.out
@@ -3,13 +3,13 @@
   Imported 'Int'
   Set: pp::unicode
 3 | 6
-true
-false
-true
-true
+3 | 6
+3 | 7
+2 | 6
+1 | 6
   Assumed: x
-3 + -1 * (x * (3 div x)) = 0
-x + -1 * (3 * (x div 3)) = 0
-false
+x | 3
+3 | x
+6 | 3
   Set: lean::pp::notation
 Int::divides 3 x
diff --git a/tests/lean/arith7.lean b/tests/lean/arith7.lean
index 9a3606615..a24d198be 100644
--- a/tests/lean/arith7.lean
+++ b/tests/lean/arith7.lean
@@ -1,15 +1,15 @@
 import Int.
-eval | -2 |
+check | -2 |
 
 -- Unfortunately, we can't write |-2|, because |- is considered a single token.
 -- It is not wise to change that since the symbol |- can be used as the notation for
 -- entailment relation in Lean.
 eval |3|
 definition x : Int := -3
-eval |x + 1|
-eval |x + 1| > 0
+check |x + 1|
+check |x + 1| > 0
 variable y : Int
-eval |x + y|
+check |x + y|
 print |x + y| > x
 set_option pp::notation false
 print |x + y| > x
diff --git a/tests/lean/arith7.lean.expected.out b/tests/lean/arith7.lean.expected.out
index cf0d53e10..6c03b71d1 100644
--- a/tests/lean/arith7.lean.expected.out
+++ b/tests/lean/arith7.lean.expected.out
@@ -1,14 +1,13 @@
   Set: pp::colors
   Set: pp::unicode
   Imported 'Int'
-eps (nonempty_intro -2) (λ r : ℤ, ((⊥ → r = -2) → (⊤ → r = 2) → ⊥) → ⊥)
-3
+| -2 | : ℤ
+| 3 |
   Defined: x
-eps (nonempty_intro -2) (λ r : ℤ, ((⊥ → r = -2) → (⊤ → r = 2) → ⊥) → ⊥)
-eps (nonempty_intro -2) (λ r : ℤ, ((⊥ → r = -2) → (⊤ → r = 2) → ⊥) → ⊥) ≤ 0 → ⊥
+| x + 1 | : ℤ
+| x + 1 | > 0 : Bool
   Assumed: y
-eps (nonempty_intro (-3 + y))
-    (λ r : ℤ, ((0 ≤ -3 + y → r = -3 + y) → ((0 ≤ -3 + y → ⊥) → r = -1 * (-3 + y)) → ⊥) → ⊥)
+| x + y | : ℤ
 | x + y | > x
   Set: lean::pp::notation
 Int::gt (Int::abs (Int::add x y)) x
diff --git a/tests/lean/cond_tac.lean b/tests/lean/cond_tac.lean
index dbdd86820..e592e7065 100644
--- a/tests/lean/cond_tac.lean
+++ b/tests/lean/cond_tac.lean
@@ -27,12 +27,6 @@ theorem T2 (a b : Bool) : a -> a ∨ b.
   (* simple_tac *)
   done
 
-definition x := 10
-theorem T3 : x + 20 +2 >= 2*x.
-  (* eval_tac() *)
-  (* trivial_tac() *)
-  done
-
 theorem T4 (a b c : Bool) : a -> b -> c -> a ∧ b.
   (* simple2_tac *)
   exact
diff --git a/tests/lean/cond_tac.lean.expected.out b/tests/lean/cond_tac.lean.expected.out
index 0646e0988..9a2d840db 100644
--- a/tests/lean/cond_tac.lean.expected.out
+++ b/tests/lean/cond_tac.lean.expected.out
@@ -5,8 +5,6 @@ Cond result: true
   Proved: T1
 Cond result: false
   Proved: T2
-  Defined: x
-  Proved: T3
 When result: true
   Proved: T4
 When result: false
diff --git a/tests/lean/eq4.lean.expected.out b/tests/lean/eq4.lean.expected.out
index adbf26673..c860de901 100644
--- a/tests/lean/eq4.lean.expected.out
+++ b/tests/lean/eq4.lean.expected.out
@@ -2,5 +2,5 @@
   Set: pp::unicode
   Imported 'Int'
   Imported 'Real'
-⊤
-⊤
+1 = 1
+1 = 1
diff --git a/tests/lean/find.lean.expected.out b/tests/lean/find.lean.expected.out
index 875c5f8ed..a823e00e3 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 B : TypeU} {f g : A → B} (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 B : (Type U)} {f g : A → B} (a : A) (H : f = g) : f a = g a
+theorem congr2 {A B : (Type U)} {a b : A} (f : A → B) (H : a = b) : f a = f b
+theorem congr {A B : (Type U)} {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/lua11.lean b/tests/lean/lua11.lean
index 0f6f2247b..3c913a025 100644
--- a/tests/lean/lua11.lean
+++ b/tests/lean/lua11.lean
@@ -38,7 +38,7 @@ import Int.
  assert(env:find_object("val"):get_weight() == 1)
  assert(env:find_object("congr"):is_opaque())
  assert(env:find_object("congr"):is_theorem())
- assert(env:find_object("refl"):is_axiom())
+ assert(env:find_object("hrefl"):is_axiom())
  assert(env:find_object(name("Int", "sub")):is_definition())
  assert(env:find_object("x"):is_var_decl())
 *)
diff --git a/tests/lean/map.lean.expected.out b/tests/lean/map.lean.expected.out
index 165af9ac7..0d5e86eb1 100644
--- a/tests/lean/map.lean.expected.out
+++ b/tests/lean/map.lean.expected.out
@@ -9,6 +9,7 @@
   Assumed: map_nil
 Visit, depth: 1, map (λ x : ℕ, x + 1) (cons 1 (cons 2 nil)) = cons 2 (cons 3 nil)
 Visit, depth: 2, @eq
+Step: @eq ===> @eq
 Visit, depth: 2, map (λ x : ℕ, x + 1) (cons 1 (cons 2 nil))
 Visit, depth: 3, @map
 Step: @map ===> @map
@@ -64,5 +65,6 @@ Step: map (λ x : ℕ, x + 1) (cons 1 (cons 2 nil)) ===> cons 2 (cons 3 nil)
 Rewrite using: eq_id
   cons 2 (cons 3 nil) = cons 2 (cons 3 nil) ===> ⊤
 Visit, depth: 2, ⊤
+Step: ⊤ ===> ⊤
 Step: map (λ x : ℕ, x + 1) (cons 1 (cons 2 nil)) = cons 2 (cons 3 nil) ===> ⊤
   Proved: T1
diff --git a/tests/lean/norm_tac.lean b/tests/lean/norm_tac.lean
index 49367f870..aede4d619 100644
--- a/tests/lean/norm_tac.lean
+++ b/tests/lean/norm_tac.lean
@@ -6,7 +6,9 @@ set_option pp::notation false
 variable vector (A : Type) (sz : Nat) : Type
 variable read {A : Type} {sz : Nat} (v : vector A sz) (i : Nat) (H : i < sz) : A
 variable V1 : vector Int 10
-definition D := read V1 1 (by trivial)
+axiom H : 1 < 10
+add_rewrite H
+definition D := read V1 1 (by simp)
 print environment 1
 variable b : Bool
 definition a := b
diff --git a/tests/lean/norm_tac.lean.expected.out b/tests/lean/norm_tac.lean.expected.out
index 77c67417f..807b621d4 100644
--- a/tests/lean/norm_tac.lean.expected.out
+++ b/tests/lean/norm_tac.lean.expected.out
@@ -8,8 +8,9 @@
   Assumed: vector
   Assumed: read
   Assumed: V1
+  Assumed: H
   Defined: D
-definition D : ℤ := @read ℤ 10 V1 1 trivial
+definition D : ℤ := @read ℤ 10 V1 1 (@eqt_elim (Nat::lt 1 10) (@refl Bool ⊤))
   Assumed: b
   Defined: a
   Proved: T
diff --git a/tests/lean/revapp.lean b/tests/lean/revapp.lean
index c552cdc40..c88e0d89b 100644
--- a/tests/lean/revapp.lean
+++ b/tests/lean/revapp.lean
@@ -2,29 +2,27 @@ import Int.
 definition revapp {A : (Type U)} {B : A -> (Type U)} (a : A) (f : forall (x : A), B x) : (B a) := f a.
 infixl 100 |> : revapp
 
-eval 10 |> (fun x, x + 1)
-        |> (fun x, x + 2)
-        |> (fun x, 2 * x)
-        |> (fun x, 3 - x)
-        |> (fun x, x + 2)
+check 10 |> (fun x, x + 1)
+         |> (fun x, x + 2)
+         |> (fun x, 2 * x)
+         |> (fun x, 3 - x)
+         |> (fun x, x + 2)
 
 definition revcomp {A B C: (Type U)} (f : A -> B) (g : B -> C) : A -> C :=
         fun x, g (f x)
 infixl 100 #> : revcomp
 
-eval (fun x, x + 1)     #>
-     (fun x, 2 * x * x) #>
-     (fun x, 10 + x)
+check (fun x, x + 1)     #>
+      (fun x, 2 * x * x) #>
+      (fun x, 10 + x)
 
 definition simple := (fun x, x + 1)     #>
                      (fun x, 2 * x * x) #>
                      (fun x, 10 + x)
 
 check simple
-eval simple 10
 
 definition simple2 := (fun x : Int, x + 1) #>
                       (fun x, 2 * x * x)   #>
                       (fun x, 10 + x)
 check simple2
-eval simple2 (-10)
diff --git a/tests/lean/revapp.lean.expected.out b/tests/lean/revapp.lean.expected.out
index 18cae24d0..e0773c40c 100644
--- a/tests/lean/revapp.lean.expected.out
+++ b/tests/lean/revapp.lean.expected.out
@@ -2,12 +2,11 @@
   Set: pp::unicode
   Imported 'Int'
   Defined: revapp
--21
+10 |> (λ x : ℕ, x + 1) |> (λ x : ℕ, x + 2) |> (λ x : ℕ, 2 * x) |> (λ x : ℕ, 3 - x) |> (λ x : ℤ, x + 2) :
+    (λ x : ℤ, ℤ) (10 |> (λ x : ℕ, x + 1) |> (λ x : ℕ, x + 2) |> (λ x : ℕ, 2 * x) |> (λ x : ℕ, 3 - x))
   Defined: revcomp
-λ x : ℕ, 10 + 2 * (x + 1) * (x + 1)
+(λ x : ℕ, x + 1) #> (λ x : ℕ, 2 * x * x) #> (λ x : ℕ, 10 + x) : ℕ → ℕ
   Defined: simple
 simple : ℕ → ℕ
-252
   Defined: simple2
 simple2 : ℤ → ℤ
-172
diff --git a/tests/lean/rs.lean.expected.out b/tests/lean/rs.lean.expected.out
index 9de9a95e3..79db23df8 100644
--- a/tests/lean/rs.lean.expected.out
+++ b/tests/lean/rs.lean.expected.out
@@ -2,22 +2,22 @@
   Set: pp::unicode
   Assumed: bracket
   Assumed: bracket_eq
-not_false : ¬ ⊥ ↔ ⊤
-not_true : ¬ ⊤ ↔ ⊥
+not_false : (¬ ⊥) = ⊤
+not_true : (¬ ⊤) = ⊥
 Nat::mul_comm : ∀ a b : ℕ, a * b = b * a
 Nat::add_assoc : ∀ a b c : ℕ, a + b + c = a + (b + c)
 Nat::add_comm : ∀ a b : ℕ, a + b = b + a
 Nat::add_zeror : ∀ a : ℕ, a + 0 = a
-forall_rem [check] : ∀ (A : TypeU) (H : nonempty A) (p : Bool), (A → p) ↔ p
-eq_id : ∀ (A : TypeU) (a : A), a = a ↔ ⊤
-exists_rem : ∀ (A : TypeU) (H : nonempty A) (p : Bool), (∃ x : A, p) ↔ p
+forall_rem [check] : ∀ (A : TypeU) (H : inhabited A) (p : Bool), (A → p) ↔ p
+eq_id : ∀ (A : (Type U)) (a : A), a = a ↔ ⊤
+exists_rem : ∀ (A : TypeU) (H : inhabited A) (p : Bool), (∃ x : A, p) ↔ p
 exists_and_distributel : ∀ (A : TypeU) (p : Bool) (φ : A → Bool),
       (∃ x : A, φ x ∧ p) ↔ (∃ x : A, φ x) ∧ p
 exists_or_distribute : ∀ (A : TypeU) (φ ψ : A → Bool),
       (∃ x : A, φ x ∨ ψ x) ↔ (∃ x : A, φ x) ∨ (∃ x : A, ψ x)
 not_and : ∀ a b : Bool, ¬ (a ∧ b) ↔ ¬ a ∨ ¬ b
 not_neq : ∀ (A : TypeU) (a b : A), ¬ a ≠ b ↔ a = b
-not_true : ¬ ⊤ ↔ ⊥
+not_true : (¬ ⊤) = ⊥
 and_comm : ∀ a b : Bool, a ∧ b ↔ b ∧ a
 and_truer : ∀ a : Bool, a ∧ ⊤ ↔ a
 bracket_eq [check] : ∀ a : Bool, bracket a = a
diff --git a/tests/lean/scope.lean.expected.out b/tests/lean/scope.lean.expected.out
index 6d58b8c31..d4c08cd2c 100644
--- a/tests/lean/scope.lean.expected.out
+++ b/tests/lean/scope.lean.expected.out
@@ -28,4 +28,4 @@ theorem Inj (A B : Type)
         L4 : x = hinv (h x) := symm L2,
         L5 : x = hinv (h y) := trans L4 L1
     in trans L5 L3
-10
+20 - 10
diff --git a/tests/lean/scope_bug1.lean b/tests/lean/scope_bug1.lean
index c65eb87ce..0e0ff348e 100644
--- a/tests/lean/scope_bug1.lean
+++ b/tests/lean/scope_bug1.lean
@@ -10,9 +10,9 @@ scope
 
 theorem mul_zerol2 (a : Nat) : 0 * a = 0
 := induction_on a
-    (have 0 * 0 = 0 : trivial)
+    (have 0 * 0 = 0 : mul_zeror 0)
     (λ (n : Nat) (iH : 0 * n = 0),
         calc  0 * (n + 1)  =  (0 * n) + 0 : mul_succr 0 n
                       ...  =  0 + 0       : { iH }
-                      ...  =  0           : trivial)
+                      ...  =  0           : add_zeror 0)
 end
\ No newline at end of file
diff --git a/tests/lean/simp10.lean b/tests/lean/simp10.lean
index 482a6534e..a180800f4 100644
--- a/tests/lean/simp10.lean
+++ b/tests/lean/simp10.lean
@@ -6,6 +6,11 @@ add_rewrite fid
 axiom gcnst (x : Nat) : g x = 1
 add_rewrite gcnst
 
+theorem one_neq_0 : 1 ≠ 0
+:= Nat::succ_nz 0
+
+add_rewrite one_neq_0
+
 (*
 local t = parse_lean("f a")
 local r, pr = simplify(t)
diff --git a/tests/lean/simp10.lean.expected.out b/tests/lean/simp10.lean.expected.out
index 23ed1140c..903a56b3b 100644
--- a/tests/lean/simp10.lean.expected.out
+++ b/tests/lean/simp10.lean.expected.out
@@ -5,5 +5,8 @@
   Assumed: a
   Assumed: fid
   Assumed: gcnst
+  Proved: one_neq_0
 a
-fid a (eqt_elim (congr1 0 (congr2 neq (gcnst a))))
+fid a
+    (eqt_elim (trans (trans (congr1 0 (congr2 neq (gcnst a))) neq_to_not_eq)
+                     (trans (congr2 not (neq_elim one_neq_0)) not_false)))
diff --git a/tests/lean/simp17.lean b/tests/lean/simp17.lean
index facb8e33c..905907de5 100644
--- a/tests/lean/simp17.lean
+++ b/tests/lean/simp17.lean
@@ -1,5 +1,5 @@
 rewrite_set simple
-add_rewrite and_truer and_truel and_falser and_falsel or_falsel Nat::add_zeror : simple
+add_rewrite and_truer and_truel and_falser and_falsel or_falsel Nat::add_zeror a_neq_a : simple
 (*
   add_congr_theorem("simple", "and_congrr")
 *)
diff --git a/tests/lean/simp17.lean.expected.out b/tests/lean/simp17.lean.expected.out
index f60787845..ce3f0ca92 100644
--- a/tests/lean/simp17.lean.expected.out
+++ b/tests/lean/simp17.lean.expected.out
@@ -6,8 +6,9 @@
 ⊥
 trans (and_congrr
            (λ C::1 : b = 0 ∧ c = 1,
-              congr (congr2 neq (congr1 0 (congr2 Nat::add (and_elimr C::1))))
-                    (congr1 1 (congr2 Nat::add (and_eliml C::1))))
+              trans (congr (congr2 neq (congr1 0 (congr2 Nat::add (and_elimr C::1))))
+                           (congr1 1 (congr2 Nat::add (and_eliml C::1))))
+                    (a_neq_a 1))
            (λ C::7 : ⊥, refl (b = 0 ∧ c = 1)))
       (and_falser (b = 0 ∧ c = 1))
 (c + 0 ≠ b + 1 ∧ b = 0 ∧ c = 1) = ⊥
diff --git a/tests/lean/simp3.lean.expected.out b/tests/lean/simp3.lean.expected.out
index 3158f973d..df175dcbc 100644
--- a/tests/lean/simp3.lean.expected.out
+++ b/tests/lean/simp3.lean.expected.out
@@ -1,11 +1,11 @@
   Set: pp::colors
   Set: pp::unicode
   Defined: double
-⊤
+¬ 0 = 1
 ⊤
 9
-⊥
-2 + 2 + (2 + 2) + 1 ≥ 3
+0 = 1
+3 ≤ 2 + 2 + (2 + 2) + 1
 3 ≤ 2 * 2 + (2 * 2 + (2 * 2 + (2 * 2 + 1)))
   Assumed: a
   Assumed: b
@@ -32,4 +32,4 @@ a * a + (a * b + (b * a + b * b))
 ⊤ → ⊥	refl (⊤ → ⊥)	false
 ⊤ → ⊤	refl (⊤ → ⊤)	false
 ⊥ → ⊤	imp_congr (refl ⊥) (λ C::1 : ⊥, eqt_intro C::1)	false
-⊥	refl ⊥	false
+⊤ ↔ ⊥	refl (⊤ ↔ ⊥)	false
diff --git a/tests/lean/simp33.lean b/tests/lean/simp33.lean
index 6baaf595d..40d1c98dc 100644
--- a/tests/lean/simp33.lean
+++ b/tests/lean/simp33.lean
@@ -3,7 +3,7 @@ variable f {A : TypeU} : A → A
 axiom Ax1 (a : Bool) : f a = not a
 axiom Ax2 (a : Nat)  : f a = 0
 rewrite_set S
-add_rewrite Ax1 Ax2 : S
+add_rewrite Ax1 Ax2 not_false : S
 theorem T1 (a : Nat) : f (f a > 0)
 := by simp S
 print environment 1
diff --git a/tests/lean/simp33.lean.expected.out b/tests/lean/simp33.lean.expected.out
index 548ef0bd1..224c905c1 100644
--- a/tests/lean/simp33.lean.expected.out
+++ b/tests/lean/simp33.lean.expected.out
@@ -5,4 +5,5 @@
   Assumed: Ax1
   Assumed: Ax2
   Proved: T1
-theorem T1 (a : ℕ) : f (f a > 0) := eqt_elim (trans (congr2 f (congr1 0 (congr2 Nat::gt (Ax2 a)))) (Ax1 ⊥))
+theorem T1 (a : ℕ) : f (f a > 0) :=
+    eqt_elim (trans (trans (congr2 f (congr1 0 (congr2 Nat::gt (Ax2 a)))) (Ax1 ⊥)) not_false)
diff --git a/tests/lean/tst1.lean.expected.out b/tests/lean/tst1.lean.expected.out
index 8613cfa3a..219860a93 100644
--- a/tests/lean/tst1.lean.expected.out
+++ b/tests/lean/tst1.lean.expected.out
@@ -25,7 +25,7 @@ definition select {A : Type} {n : N} (v : vector A n) (i : N) (H : i < n) : A :=
 definition map {A B C : Type} {n : N} (f : A → B → C) (v1 : vector A n) (v2 : vector B n) : vector C n :=
     λ (i : N) (H : i < n), f (v1 i H) (v2 i H)
 select (update (const three ⊥) two ⊤) two two_lt_three : Bool
-eps (nonempty_intro ⊤) (λ r : Bool, ((two = two → r = ⊤) → ((two = two → ⊥) → r = ⊥) → ⊥) → ⊥)
+if two = two then ⊤ else ⊥
 update (const three ⊥) two ⊤ : vector Bool three
 
 --------
@@ -45,5 +45,4 @@ map normal form -->
   f (v1 i H) (v2 i H)
 
 update normal form --> 
-λ (A : Type) (n : N) (v : ∀ (i : N), i < n → A) (i : N) (d : A) (j : N) (H : j < n),
-  eps (nonempty_intro d) (λ r : A, ((j = i → r = d) → ((j = i → ⊥) → r = v j H) → ⊥) → ⊥)
+λ (A : Type) (n : N) (v : ∀ (i : N), i < n → A) (i : N) (d : A) (j : N) (H : j < n), if j = i then d else v j H
diff --git a/tests/lean/tst11.lean b/tests/lean/tst11.lean
index 67e2da3cd..25676cc61 100644
--- a/tests/lean/tst11.lean
+++ b/tests/lean/tst11.lean
@@ -1,12 +1,13 @@
+import tactic
 definition xor (x y : Bool) : Bool := (not x) = y
 infixr 50 ⊕ : xor
 print xor true false
-eval xor true true
-eval xor true false
 variable a : Bool
 print a ⊕ a ⊕ a
 check @subst
 theorem EM2 (a : Bool) : a \/ (not a) :=
-   case (fun x : Bool, x \/ (not x)) trivial trivial a
+   case (fun x : Bool, x \/ (not x)) (by simp) (by simp) a
 check EM2
 check EM2 a
+theorem xor_neq (a b : Bool) : (a ⊕ b) ↔ ((¬ a) = b)
+:= refl (a ⊕ b)
\ No newline at end of file
diff --git a/tests/lean/tst11.lean.expected.out b/tests/lean/tst11.lean.expected.out
index 02af3b075..74a97ae2f 100644
--- a/tests/lean/tst11.lean.expected.out
+++ b/tests/lean/tst11.lean.expected.out
@@ -1,12 +1,12 @@
   Set: pp::colors
   Set: pp::unicode
+  Imported 'tactic'
   Defined: xor
 ⊤ ⊕ ⊥
-⊥
-⊤
   Assumed: a
 a ⊕ a ⊕ a
-@subst : ∀ (A : TypeU) (a b : A) (P : A → Bool), P a → a = b → P b
+@subst : ∀ (A : (Type U)) (a b : A) (P : A → Bool), P a → a = b → P b
   Proved: EM2
 EM2 : ∀ a : Bool, a ∨ ¬ a
 EM2 a : a ∨ ¬ a
+  Proved: xor_neq
diff --git a/tests/lean/tst12.lean.expected.out b/tests/lean/tst12.lean.expected.out
index 6aaf0e525..36e123104 100644
--- a/tests/lean/tst12.lean.expected.out
+++ b/tests/lean/tst12.lean.expected.out
@@ -6,4 +6,4 @@ let x := ⊤,
     z := x ∧ y,
     f := λ arg1 arg2 : Bool, arg1 ∧ arg2 = arg2 ∧ arg1 = arg1 ∨ arg2 ∨ arg2
 in f x y ∨ z
-⊤
+(⊤ ∧ ⊤ = ⊤ ∧ ⊤ = ⊤ ∨ ⊤ ∨ ⊤) ∨ ⊤ ∧ ⊤
diff --git a/tests/lean/tst17.lean.expected.out b/tests/lean/tst17.lean.expected.out
index 81e287196..ea412f86a 100644
--- a/tests/lean/tst17.lean.expected.out
+++ b/tests/lean/tst17.lean.expected.out
@@ -4,4 +4,4 @@
   Assumed: g
 ∀ a b : Type, ∃ c : Type, g a b = f c
 ∀ a b : Type, ∃ c : Type, g a b = f c : Bool
-∀ (a b : Type), (∀ (x : Type), g a b = f x → ⊥) → ⊥
+∀ a b : Type, ∃ c : Type, g a b = f c
diff --git a/tests/lean/tst4.lean.expected.out b/tests/lean/tst4.lean.expected.out
index 6201629bc..6f6deefa8 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 : (Type U)) (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
diff --git a/tests/lean/using_bug1.lean b/tests/lean/using_bug1.lean
index 000525919..98abbfe75 100644
--- a/tests/lean/using_bug1.lean
+++ b/tests/lean/using_bug1.lean
@@ -8,8 +8,8 @@ check add_succr a
 
 theorem mul_zerol2 (a : Nat) : 0 * a = 0
 := induction_on a
-    (have 0 * 0 = 0 : trivial)
+    (have 0 * 0 = 0 : mul_zeror 0)
     (λ (n : Nat) (iH : 0 * n = 0),
         calc  0 * (n + 1)  =  (0 * n) + 0 : mul_succr 0 n
                       ...  =  0 + 0       : { iH }
-                      ...  =  0           : trivial)
+                      ...  =  0           : add_zeror 0)
diff --git a/tests/lua/env4.lua b/tests/lua/env4.lua
index be3ffef34..62cfdc34c 100644
--- a/tests/lua/env4.lua
+++ b/tests/lua/env4.lua
@@ -26,7 +26,7 @@ assert(not ok)
 print(msg)
 assert(child:normalize(Const("val2")) == Const("val2"))
 local Int = Const("Int")
-child:add_theorem("Th1", mk_eq(Int, iVal(0), iVal(0)), Const("trivial"))
+child:add_theorem("Th1", mk_eq(Int, iVal(0), iVal(0)), Const("refl")(Int, iVal(0)))
 child:add_axiom("H1", mk_eq(Int, Const("x"), iVal(0)))
 assert(child:has_object("H1"))
 local ctx = context(context(), "x", Const("Int"), iVal(10))