diff --git a/src/builtin/Nat.lean b/src/builtin/Nat.lean
index e2408ba85..f1c042d0c 100644
--- a/src/builtin/Nat.lean
+++ b/src/builtin/Nat.lean
@@ -36,7 +36,7 @@ axiom add_zeror (a : Nat)   : a + 0 = a
 axiom add_succr (a b : Nat) : a + (b + 1) = (a + b) + 1
 axiom mul_zeror (a : Nat)    : a * 0 = 0
 axiom mul_succr (a b : Nat)  : a * (b + 1) = a * b + a
-axiom le_def (a b : Nat) : a ≤ b ⟷ ∃ c, a + c = b
+axiom le_def (a b : Nat) : a ≤ b ↔ ∃ c, a + c = b
 axiom induction {P : Nat → Bool} (H1 : P 0) (H2 : ∀ (n : Nat) (iH : P n), P (n + 1)) : ∀ a, P a
 
 theorem induction_on {P : Nat → Bool} (a : Nat) (H1 : P 0) (H2 : ∀ (n : Nat) (iH : P n), P (n + 1)) : P a
diff --git a/src/builtin/cast.lean b/src/builtin/cast.lean
index f89d052a0..e95a68624 100644
--- a/src/builtin/cast.lean
+++ b/src/builtin/cast.lean
@@ -45,7 +45,7 @@ theorem hcongr
        L3 : b == b'                     := cast_eq L2 b,
        L4 : a == b'                     := htrans H2 L3,
        L5 : f a == f b'                 := congr2 f L4,
-       S1 : (∀ x, B' x) == (∀ x, B x)   := symm (type_eq H1),
+       S1 : (∀ x, B' x) == (∀ x, B x)  := symm (type_eq H1),
        g' : (∀ x, B x)                  := cast S1 g,
        L6 : g == g'                     := cast_eq S1 g,
        L7 : f == g'                     := htrans H1 L6,
@@ -54,6 +54,17 @@ theorem hcongr
       L10 : g' b' == g b                := cast_app S1 L2 g b
    in htrans L9 L10
 
+theorem hfunext
+     {A : TypeM} {B B' : A → TypeM} {f : ∀ x : A, B x} {g : ∀ x : A, B' x} (H : ∀ x : A, f x == g x) : f == g
+:= let L1   : (∀ x : A, B x = B' x)             := λ x : A, type_eq (H x),
+       L2   : (∀ x : A, B x) = (∀ x : A, B' x) := allext L1,
+       g'   : (∀ x : A, B x)                    := cast (symm L2) g,
+       Hgg  : g == g'                            := cast_eq (symm L2) g,
+       Hggx : (∀ x : A, g x == g' x)            := λ x : A, hcongr Hgg (refl x) ,
+       L3   : (∀ x : A, f x == g' x)            := λ x : A, htrans (H x) (Hggx x),
+       Hfg  : f == g'                            := funext L3
+   in htrans Hfg (hsymm Hgg)
+
 exit -- Stop here, the following axiom is not sound
 
 -- The following axiom is unsound when we treat Pi and
diff --git a/src/builtin/kernel.lean b/src/builtin/kernel.lean
index 8fb67f3c1..a524307ce 100644
--- a/src/builtin/kernel.lean
+++ b/src/builtin/kernel.lean
@@ -30,7 +30,7 @@ definition implies (a b : Bool) := a → b
 definition iff (a b : Bool) := a == b
 
 infixr 25 <-> : iff
-infixr 25 ⟷  : iff
+infixr 25 ↔   : iff
 
 -- The Lean parser has special treatment for the constant exists.
 -- It allows us to write
@@ -103,8 +103,8 @@ theorem imp_eq_trans {a b c : Bool} (H1 : a → b) (H2 : b = c) : a → c
 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
+theorem not_not_eq (a : Bool) : ¬ ¬ a ↔ a
+:= case (λ x, ¬ ¬ x ↔ x) trivial trivial a
 
 theorem not_not_elim {a : Bool} (H : ¬ ¬ a) : a
 := (not_not_eq a) ◂ H
@@ -174,6 +174,16 @@ theorem eq_ne_trans {A : TypeU} {a b c : A} (H1 : a = b) (H2 : b ≠ c) : a ≠
 theorem ne_eq_trans {A : TypeU} {a b c : A} (H1 : a ≠ b) (H2 : b = c) : a ≠ c
 := subst H1 H2
 
+theorem heq_congr {A : TypeU} {a b c d : A} (H1 : a == c) (H2 : b == d) : (a == b) = (c == d)
+:= calc (a == b) = (c == b) : { H1 }
+             ... = (c == d) : { H2 }
+
+theorem heq_congrl {A : TypeU} {a : A} (b : A) {c : A} (H : a == c) : (a == b) = (c == b)
+:= heq_congr H (refl b)
+
+theorem heq_congrr {A : TypeU} (a : A) {b d : A} (H : b == d) : (a == b) = (a == d)
+:= heq_congr (refl a) H
+
 theorem eqt_elim {a : Bool} (H : a = true) : a
 := (symm H) ◂ trivial
 
@@ -228,14 +238,14 @@ 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
+theorem neq_elim {A : TypeU} {a b : A} (H : a ≠ b) : a = b ↔ false
 := eqf_intro H
 
-theorem or_comm (a b : Bool) : a ∨ b ⟷ b ∨ a
+theorem or_comm (a b : Bool) : a ∨ b ↔ b ∨ a
 := boolext (assume H, or_elim H (λ H1, or_intror b H1) (λ H2, or_introl H2 a))
            (assume H, or_elim H (λ H1, or_intror a H1) (λ H2, or_introl H2 b))
 
-theorem or_assoc (a b c : Bool) : (a ∨ b) ∨ c ⟷ a ∨ (b ∨ c)
+theorem or_assoc (a b c : Bool) : (a ∨ b) ∨ c ↔ a ∨ (b ∨ c)
 := boolext (assume H : (a ∨ b) ∨ c,
                       or_elim H (λ H1 : a ∨ b, or_elim H1 (λ Ha : a, or_introl Ha (b ∨ c))
                                                           (λ Hb : b, or_intror a (or_introl Hb c)))
@@ -245,118 +255,118 @@ theorem or_assoc (a b c : Bool) : (a ∨ b) ∨ c ⟷ a ∨ (b ∨ c)
                                 (λ H1 : b ∨ c, or_elim H1 (λ Hb : b, or_introl (or_intror a Hb) c)
                                                           (λ Hc : c, or_intror (a ∨ b) Hc)))
 
-theorem or_id (a : Bool) : a ∨ a ⟷ a
+theorem or_id (a : Bool) : a ∨ a ↔ a
 := boolext (assume H, or_elim H (λ H1, H1) (λ H2, H2))
            (assume H, or_introl H a)
 
-theorem or_falsel (a : Bool) : a ∨ false ⟷ a
+theorem or_falsel (a : Bool) : a ∨ false ↔ a
 := boolext (assume H, or_elim H (λ H1, H1) (λ H2, false_elim a H2))
            (assume H, or_introl H false)
 
-theorem or_falser (a : Bool) : false ∨ a ⟷ a
+theorem or_falser (a : Bool) : false ∨ a ↔ a
 := (or_comm false a) ⋈ (or_falsel a)
 
-theorem or_truel (a : Bool) : true ∨ a ⟷ true
+theorem or_truel (a : Bool) : true ∨ a ↔ true
 := eqt_intro (case (λ x : Bool, true ∨ x) trivial trivial a)
 
-theorem or_truer (a : Bool) : a ∨ true ⟷ true
+theorem or_truer (a : Bool) : a ∨ true ↔ true
 := (or_comm a true) ⋈ (or_truel a)
 
-theorem or_tauto (a : Bool) : a ∨ ¬ a ⟷ true
+theorem or_tauto (a : Bool) : a ∨ ¬ a ↔ true
 := eqt_intro (em a)
 
-theorem and_comm (a b : Bool) : a ∧ b ⟷ b ∧ a
+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))
 
-theorem and_id (a : Bool) : a ∧ a ⟷ a
+theorem and_id (a : Bool) : a ∧ a ↔ a
 := boolext (assume H, and_eliml H)
            (assume H, and_intro H H)
 
-theorem and_assoc (a b c : Bool) : (a ∧ b) ∧ c ⟷ a ∧ (b ∧ c)
+theorem and_assoc (a b c : Bool) : (a ∧ b) ∧ c ↔ a ∧ (b ∧ c)
 := boolext (assume H, and_intro (and_eliml (and_eliml H)) (and_intro (and_elimr (and_eliml H)) (and_elimr H)))
            (assume H, and_intro (and_intro (and_eliml H) (and_eliml (and_elimr H))) (and_elimr (and_elimr H)))
 
-theorem and_truer (a : Bool) : a ∧ true ⟷ a
+theorem and_truer (a : Bool) : a ∧ true ↔ a
 := boolext (assume H : a ∧ true,  and_eliml H)
            (assume H : a,         and_intro H trivial)
 
-theorem and_truel (a : Bool) : true ∧ a ⟷ a
+theorem and_truel (a : Bool) : true ∧ a ↔ a
 := trans (and_comm true a) (and_truer a)
 
-theorem and_falsel (a : Bool) : a ∧ false ⟷ false
+theorem and_falsel (a : Bool) : a ∧ false ↔ false
 := boolext (assume H, and_elimr H)
            (assume H, false_elim (a ∧ false) H)
 
-theorem and_falser (a : Bool) : false ∧ a ⟷ false
+theorem and_falser (a : Bool) : false ∧ a ↔ false
 := (and_comm false a) ⋈ (and_falsel a)
 
-theorem and_absurd (a : Bool) : a ∧ ¬ a ⟷ false
+theorem and_absurd (a : Bool) : a ∧ ¬ a ↔ false
 := boolext (assume H, absurd (and_eliml H) (and_elimr H))
            (assume H, false_elim (a ∧ ¬ a) H)
 
-theorem imp_truer (a : Bool) : (a → true) ⟷ true
-:= case (λ x, (x → true) ⟷ true) trivial trivial a
+theorem imp_truer (a : Bool) : (a → true) ↔ true
+:= case (λ x, (x → true) ↔ true) trivial trivial a
 
-theorem imp_truel (a : Bool) : (true → a) ⟷ a
-:= case (λ x, (true → x) ⟷ x) trivial trivial a
+theorem imp_truel (a : Bool) : (true → a) ↔ a
+:= case (λ x, (true → x) ↔ x) trivial trivial a
 
-theorem imp_falser (a : Bool) : (a → false) ⟷ ¬ a
+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
+theorem imp_falsel (a : Bool) : (false → a) ↔ true
+:= case (λ x, (false → x) ↔ true) trivial trivial a
 
-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)
+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)
+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)
+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
+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)
+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
+theorem not_congr {a b : Bool} (H : a ↔ b) : ¬ a ↔ ¬ b
 := congr2 not H
 
-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)
+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)
+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 not_exists (A : (Type U)) (P : A → Bool) : ¬ (∃ x : A, P x) ⟷ (∀ x : A, ¬ P x)
+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)
                      ... = ∀ x : A, ¬ P x     : not_not_eq (∀ x : A, ¬ P x)
 
@@ -378,7 +388,7 @@ theorem exists_unfold2 {A : TypeU} {P : A → Bool} (a : A) (H : P a ∨ (∃ x
                (λ (w : A) (Hw : w ≠ a ∧ P w),
                   exists_intro w (and_elimr Hw)))
 
-theorem exists_unfold {A : TypeU} (P : A → Bool) (a : A) : (∃ x : A, P x) ⟷ (P a ∨ (∃ x : A, x ≠ a ∧ P x))
+theorem exists_unfold {A : TypeU} (P : A → Bool) (a : A) : (∃ x : A, P x) ↔ (P a ∨ (∃ x : 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)
 
@@ -390,10 +400,10 @@ theorem left_comm {A : TypeU} {R : A -> A -> A} (comm : ∀ x y, R x y = R y x)
                          ...    = R (R y x) z : { comm x y }
                          ...    = R y (R x z) : assoc y x z
 
-theorem and_left_comm (a b c : Bool) : a ∧ (b ∧ c) ⟷ b ∧ (a ∧ c)
+theorem and_left_comm (a b c : Bool) : a ∧ (b ∧ c) ↔ b ∧ (a ∧ c)
 := left_comm and_comm and_assoc a b c
 
-theorem or_left_comm (a b c : Bool) : a ∨ (b ∨ c) ⟷ b ∨ (a ∨ c)
+theorem or_left_comm (a b c : Bool) : a ∨ (b ∨ c) ↔ b ∨ (a ∨ c)
 := left_comm or_comm or_assoc a b c
 
 -- Congruence theorems for contextual simplification
@@ -463,24 +473,24 @@ theorem imp_congr {a b c d : Bool} (H_ac : a = c) (H_bd : ∀ (H_c : c), b = d)
 := imp_congrr (λ H, H_ac) H_bd
 
 -- In the following theorems we are using the fact that a ∨ b is defined as ¬ a → b
-theorem or_congrr {a b c d : Bool} (H_ac : ∀ (H_nb : ¬ b), a = c) (H_bd : ∀ (H_nc : ¬ c), b = d) : a ∨ b ⟷ c ∨ d
+theorem or_congrr {a b c d : Bool} (H_ac : ∀ (H_nb : ¬ b), a = c) (H_bd : ∀ (H_nc : ¬ c), b = d) : a ∨ b ↔ c ∨ d
 := imp_congrr (λ H_nb : ¬ b, congr2 not (H_ac H_nb)) H_bd
-theorem or_congrl {a b c d : Bool} (H_ac : ∀ (H_nd : ¬ d), a = c) (H_bd : ∀ (H_na : ¬ a), b = d) : a ∨ b ⟷ c ∨ d
+theorem or_congrl {a b c d : Bool} (H_ac : ∀ (H_nd : ¬ d), a = c) (H_bd : ∀ (H_na : ¬ a), b = d) : a ∨ b ↔ c ∨ d
 := imp_congrl (λ H_nd : ¬ d, congr2 not (H_ac H_nd)) H_bd
 -- (Common case) simplify a to c, and then b to d using the fact that ¬ c is true
-theorem or_congr {a b c d : Bool} (H_ac : a = c) (H_bd : ∀ (H_nc : ¬ c), b = d) : a ∨ b ⟷ c ∨ d
+theorem or_congr {a b c d : Bool} (H_ac : a = c) (H_bd : ∀ (H_nc : ¬ c), b = d) : a ∨ b ↔ c ∨ d
 := or_congrr (λ H, H_ac) H_bd
 
 -- In the following theorems we are using the fact hat a ∧ b is defined as ¬ (a → ¬ b)
-theorem and_congrr {a b c d : Bool} (H_ac : ∀ (H_b : b), a = c) (H_bd : ∀ (H_c : c), b = d) : a ∧ b ⟷ c ∧ d
+theorem and_congrr {a b c d : Bool} (H_ac : ∀ (H_b : b), a = c) (H_bd : ∀ (H_c : c), b = d) : a ∧ b ↔ c ∧ d
 := congr2 not (imp_congrr (λ (H_nnb : ¬ ¬ b), H_ac (not_not_elim H_nnb)) (λ H_c : c, congr2 not (H_bd H_c)))
-theorem and_congrl {a b c d : Bool} (H_ac : ∀ (H_d : d), a = c) (H_bd : ∀ (H_a : a), b = d) : a ∧ b ⟷ c ∧ d
+theorem and_congrl {a b c d : Bool} (H_ac : ∀ (H_d : d), a = c) (H_bd : ∀ (H_a : a), b = d) : a ∧ b ↔ c ∧ d
 := congr2 not (imp_congrl (λ (H_nnd : ¬ ¬ d), H_ac (not_not_elim H_nnd)) (λ H_a : a, congr2 not (H_bd H_a)))
 -- (Common case) simplify a to c, and then b to d using the fact that c is true
-theorem and_congr {a b c d : Bool} (H_ac : a = c) (H_bd : ∀ (H_c : c), b = d) : a ∧ b ⟷ c ∧ d
+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 forall_or_distributer {A : TypeU} (p : Bool) (φ : A → Bool) : (∀ x, p ∨ φ x) ⟷ p ∨ ∀ x, φ x
+theorem forall_or_distributer {A : TypeU} (p : Bool) (φ : A → Bool) : (∀ x, p ∨ φ x) ↔ p ∨ ∀ x, φ x
 := boolext
      (assume H : (∀ x, p ∨ φ x),
         or_elim (em p)
@@ -493,19 +503,19 @@ theorem forall_or_distributer {A : TypeU} (p : Bool) (φ : A → Bool) : (∀ x,
               (λ H1 : p,          or_introl H1 (φ x))
               (λ H2 : (∀ x, φ x), or_intror p  (H2 x)))
 
-theorem forall_or_distributel {A : TypeU} (p : Bool) (φ : A → Bool) : (∀ x, φ x ∨ p) ⟷ (∀ x, φ x) ∨ p
+theorem forall_or_distributel {A : TypeU} (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)
 
-theorem forall_and_distribute {A : TypeU} (φ ψ : A → Bool) : (∀ x, φ x ∧ ψ x) ⟷ (∀ x, φ x) ∧ (∀ x, ψ x)
+theorem forall_and_distribute {A : TypeU} (φ ψ : A → Bool) : (∀ x, φ x ∧ ψ x) ↔ (∀ x, φ x) ∧ (∀ x, ψ x)
 := boolext
      (assume H : (∀ x, φ x ∧ ψ x),
         and_intro (take x, and_eliml (H x)) (take x, and_elimr (H x)))
      (assume H : (∀ x, φ x) ∧ (∀ x, ψ x),
         take x, and_intro (and_eliml H x) (and_elimr H x))
 
-theorem exists_and_distributer {A : TypeU} (p : Bool) (φ : A → Bool) : (∃ x, p ∧ φ x) ⟷ p ∧ ∃ x, φ x
+theorem exists_and_distributer {A : TypeU} (p : Bool) (φ : A → Bool) : (∃ x, p ∧ φ x) ↔ p ∧ ∃ x, φ x
 := boolext
      (assume H : (∃ x, p ∧ φ x),
         obtain (w : A) (Hw : p ∧ φ w), from H,
@@ -514,12 +524,12 @@ 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
+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)
+theorem exists_or_distribute {A : TypeU} (φ ψ : A → Bool) : (∃ x, φ x ∨ ψ x) ↔ (∃ x, φ x) ∨ (∃ x, ψ x)
 := boolext
     (assume H : (∃ x, φ x ∨ ψ x),
         obtain (w : A) (Hw : φ w ∨ ψ w), from H,
diff --git a/src/builtin/obj/cast.olean b/src/builtin/obj/cast.olean
index e5d578d43..371229270 100644
Binary files a/src/builtin/obj/cast.olean and b/src/builtin/obj/cast.olean differ
diff --git a/src/builtin/obj/kernel.olean b/src/builtin/obj/kernel.olean
index a9ec67ca9..b8ea3249b 100644
Binary files a/src/builtin/obj/kernel.olean and b/src/builtin/obj/kernel.olean differ
diff --git a/src/kernel/kernel_decls.cpp b/src/kernel/kernel_decls.cpp
index 74ed6351a..046b726ff 100644
--- a/src/kernel/kernel_decls.cpp
+++ b/src/kernel/kernel_decls.cpp
@@ -53,6 +53,9 @@ MK_CONSTANT(trans_fn, name("trans"));
 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(heq_congr_fn, name("heq_congr"));
+MK_CONSTANT(heq_congrl_fn, name("heq_congrl"));
+MK_CONSTANT(heq_congrr_fn, name("heq_congrr"));
 MK_CONSTANT(eqt_elim_fn, name("eqt_elim"));
 MK_CONSTANT(eqf_elim_fn, name("eqf_elim"));
 MK_CONSTANT(congr1_fn, name("congr1"));
diff --git a/src/kernel/kernel_decls.h b/src/kernel/kernel_decls.h
index b77bf028c..3190b0c7a 100644
--- a/src/kernel/kernel_decls.h
+++ b/src/kernel/kernel_decls.h
@@ -151,6 +151,15 @@ inline expr mk_eq_ne_trans_th(expr const & e1, expr const & e2, expr const & e3,
 expr mk_ne_eq_trans_fn();
 bool is_ne_eq_trans_fn(expr const & e);
 inline expr mk_ne_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_ne_eq_trans_fn(), e1, e2, e3, e4, e5, e6}); }
+expr mk_heq_congr_fn();
+bool is_heq_congr_fn(expr const & e);
+inline expr mk_heq_congr_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_heq_congr_fn(), e1, e2, e3, e4, e5, e6, e7}); }
+expr mk_heq_congrl_fn();
+bool is_heq_congrl_fn(expr const & e);
+inline expr mk_heq_congrl_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_heq_congrl_fn(), e1, e2, e3, e4, e5}); }
+expr mk_heq_congrr_fn();
+bool is_heq_congrr_fn(expr const & e);
+inline expr mk_heq_congrr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_heq_congrr_fn(), e1, e2, e3, e4, e5}); }
 expr mk_eqt_elim_fn();
 bool is_eqt_elim_fn(expr const & e);
 inline expr mk_eqt_elim_th(expr const & e1, expr const & e2) { return mk_app({mk_eqt_elim_fn(), e1, e2}); }