diff --git a/examples/lean/primes.lean b/examples/lean/primes.lean
index 29eb3a0d8..167800157 100644
--- a/examples/lean/primes.lean
+++ b/examples/lean/primes.lean
@@ -11,13 +11,6 @@ import macros
 import tactic
 using Nat
 
---
--- could go in kernel
---
-
-theorem or_imp (p q : Bool) : (p ∨ q) ↔ (¬ p → q)
-:= subst (symm (imp_or (¬ p) q)) (not_not_eq p)
-
 --
 -- fundamental properties of Nat
 --
diff --git a/src/builtin/kernel.lean b/src/builtin/kernel.lean
index be3379248..7e06e7a93 100644
--- a/src/builtin/kernel.lean
+++ b/src/builtin/kernel.lean
@@ -43,12 +43,14 @@ alias ⊥ : false
 definition not (a : Bool) := a → false
 notation 40 ¬ _ : not
 
-definition or (a b : Bool) := ¬ a → b
+definition or (a b : Bool)
+:= ∀ c : Bool, (a → c) → (b → c) → c
 infixr 30 || : or
 infixr 30 \/ : or
 infixr 30 ∨  : or
 
-definition and (a b : Bool) := ¬ (a → ¬ b)
+definition and (a b : Bool)
+:= ∀ c : Bool, (a → b → c) → c
 infixr 35 && : and
 infixr 35 /\ : and
 infixr 35 ∧  : and
@@ -65,9 +67,6 @@ 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
 
@@ -102,15 +101,40 @@ 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)
 
--- 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
+:= take c : Bool,
+     assume (H1 : a → c) (H2 : b → c),
+        H1 H
 
 theorem or_intror {b : Bool} (a : Bool) (H : b) : a ∨ b
-:= assume H1 : ¬ a, H
+:= take c : Bool,
+     assume (H1 : a → c) (H2 : b → c),
+       H2 H
+
+theorem or_elim {a b c : Bool} (H1 : a ∨ b) (H2 : a → c) (H3 : b → c) : c
+:= H1 c H2 H3
 
 theorem resolve1 {a b : Bool} (H1 : a ∨ b) (H2 : ¬ a) : b
-:= H1 H2
+:= H1 b (assume Ha : a, absurd_elim b Ha H2) (assume Hb : b, Hb)
+
+theorem resolve2 {a b : Bool} (H1 : a ∨ b) (H2 : ¬ b) : a
+:= H1 a (assume Ha : a, Ha) (assume Hb : b, absurd_elim a Hb H2)
+
+theorem or_flip {a b : Bool} (H : a ∨ b) : b ∨ a
+:= take c : Bool,
+     assume (H1 : b → c) (H2 : a → c),
+       H c H2 H1
+
+theorem and_intro {a b : Bool} (H1 : a) (H2 : b) : a ∧ b
+:= take c : Bool,
+     assume H : a → b → c,
+       H H1 H2
+
+theorem and_eliml {a b : Bool} (H : a ∧ b) : a
+:= H a (assume (Ha : a) (Hb : b), Ha)
+
+theorem and_elimr {a b : Bool} (H : a ∧ b) : b
+:= H b (assume (Ha : a) (Hb : b), Hb)
 
 axiom subst {A : (Type U)} {a b : A} {P : A → Bool} (H1 : P a) (H2 : a = b) : P b
 
@@ -195,13 +219,17 @@ theorem eqf_elim {a : Bool} (H : a = false) : ¬ a
 theorem heqt_elim {a : Bool} (H : a == true) : a
 := eqt_elim (to_eq H)
 
-axiom case (P : Bool → Bool) (H1 : P true) (H2 : P false) (a : Bool) : P a
+axiom boolcomplete (a : Bool) : a = true ∨ a = false
 
-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 case (P : Bool → Bool) (H1 : P true) (H2 : P false) (a : Bool) : P a
+:= or_elim (boolcomplete a)
+     (assume Ht : a = true,  subst H1 (symm Ht))
+     (assume Hf : a = false, subst H2 (symm Hf))
+
+theorem em (a : Bool) : a ∨ ¬ a
+:= or_elim (boolcomplete a)
+     (assume Ht : a = true, or_introl (eqt_elim Ht) (¬ a))
+     (assume Hf : a = false, or_intror a (eqf_elim Hf))
 
 theorem boolcomplete_swapped (a : Bool) : a = false ∨ a = true
 := case (λ x, x = false ∨ x = true)
@@ -254,25 +282,6 @@ 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 (H3 (resolve1 H1 (mt (assume Ha : a, H2 Ha) H)))
-               H)
-
-theorem by_contradiction {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)
        (λ Hat : a = true,  or_elim (boolcomplete b)
@@ -294,6 +303,9 @@ theorem eqf_intro {a : Bool} (H : ¬ a) : a = false
 := boolext (assume H1 : a,     absurd H1 H)
            (assume H2 : false, false_elim a H2)
 
+theorem by_contradiction {a : Bool} (H : ¬ a → false) : a
+:= or_elim (em a) (λ H1 : a, H1) (λ H1 : ¬ a, false_elim a (H H1))
+
 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)
@@ -362,9 +374,6 @@ 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))
@@ -430,6 +439,17 @@ theorem imp_or (a b : Bool) : (a → b) ↔ ¬ a ∨ b
         assume Ha : a,
           resolve1 H ((symm (not_not_eq a)) ◂ Ha))
 
+theorem or_imp (a b : Bool) : a ∨ b ↔ (¬ a → b)
+:= boolext
+     (assume H : a ∨ b,
+        (or_elim H
+           (assume (Ha : a) (Hna : ¬ a), absurd_elim b Ha Hna)
+           (assume (Hb : b) (Hna : ¬ a), Hb)))
+     (assume H : ¬ a → b,
+        (or_elim (em a)
+           (assume Ha  : a,   or_introl Ha b)
+           (assume Hna : ¬ a, or_intror a (H Hna))))
+
 theorem not_congr {a b : Bool} (H : a ↔ b) : ¬ a ↔ ¬ b
 := congr2 not H
 
@@ -509,6 +529,94 @@ theorem forall_rem {A : (Type U)} (H : inhabited A) (p : Bool) : (∀ x : A, p)
     (assume Hr : p,
        take x, Hr)
 
+
+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      : congr2 (λ x, x ∧ ¬ b) (not_not_eq a)
+
+theorem and_imp (a b : Bool) : a ∧ b ↔ ¬ (a → ¬ b)
+:= have H1 : a ∧ ¬ ¬ b ↔ ¬ (a → ¬ b),
+     from symm (not_implies a (¬ b)),
+   subst H1 (not_not_eq b)
+
+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
+
+
 -- Congruence theorems for contextual simplification
 
 -- Simplify a → b, by first simplifying a to c using the fact that ¬ b is true, and then
@@ -575,105 +683,41 @@ theorem imp_congrl {a b c d : Bool} (H_bd : ∀ (H_a : a), b = d) (H_ac : ∀ (H
 theorem imp_congr {a b c d : Bool} (H_ac : a = c) (H_bd : ∀ (H_c : c), b = d) : (a → b) = (c → 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
-:= imp_congrr (λ H_nb : ¬ b, congr2 not (H_ac H_nb)) H_bd
+:= have H1 : (¬ a → b) ↔ (¬ c → d),
+     from imp_congrr (λ H_nb : ¬ b, congr2 not (H_ac H_nb)) H_bd,
+   calc (a ∨ b) = (¬ a → b)  : or_imp _ _
+            ...  = (¬ c → d)  : H1
+            ...  = c ∨ d      : symm (or_imp _ _)
+
 theorem or_congrl {a b c d : Bool} (H_bd : ∀ (H_na : ¬ a), b = d) (H_ac : ∀ (H_nd : ¬ d), a = c) : a ∨ b ↔ c ∨ d
-:= imp_congrl H_bd (λ H_nd : ¬ d, congr2 not (H_ac H_nd))
+:= have H1 : (¬ a → b) ↔ (¬ c → d),
+     from imp_congrl H_bd (λ H_nd : ¬ d, congr2 not (H_ac H_nd)),
+   calc (a ∨ b) = (¬ a → b)  : or_imp _ _
+            ...  = (¬ c → d)  : H1
+            ...  = c ∨ d      : symm (or_imp _ _)
 -- (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
 := 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
-:= congr2 not (imp_congrr (λ (H_nnb : ¬ ¬ b), H_ac (not_not_elim H_nnb)) (λ H_c : c, congr2 not (H_bd H_c)))
+:= have H1 : ¬ (a → ¬ b) ↔ ¬ (c → ¬ d),
+     from congr2 not (imp_congrr (λ (H_nnb : ¬ ¬ b), H_ac (not_not_elim H_nnb)) (λ H_c : c, congr2 not (H_bd H_c))),
+   calc (a ∧ b) = ¬ (a → ¬ b)  : and_imp _ _
+            ...  = ¬ (c → ¬ d)  : H1
+            ...  = c ∧ d        : symm (and_imp _ _)
+
 theorem and_congrl {a b c d : Bool} (H_bd : ∀ (H_a : a), b = d) (H_ac : ∀ (H_d : d), a = c) : a ∧ b ↔ c ∧ d
-:= congr2 not (imp_congrl (λ H_a : a, congr2 not (H_bd H_a)) (λ (H_nnd : ¬ ¬ d), H_ac (not_not_elim H_nnd)))
+:= have H1 : ¬ (a → ¬ b) ↔ ¬ (c → ¬ d),
+     from congr2 not (imp_congrl (λ H_a : a, congr2 not (H_bd H_a)) (λ (H_nnd : ¬ ¬ d), H_ac (not_not_elim H_nnd))),
+   calc (a ∧ b) = ¬ (a → ¬ b)  : and_imp _ _
+            ...  = ¬ (c → ¬ d)  : H1
+            ...  = c ∧ d        : symm (and_imp _ _)
+
 -- (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
 := 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      : congr2 (λ x, x ∧ ¬ b) (not_not_eq a)
-
-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 : (Type U)} (p : Bool) (φ : A → Bool) : (∀ x, p ∨ φ x) = (p ∨ ∀ x, φ x)
 := boolext
      (assume H : (∀ x, p ∨ φ x),
diff --git a/src/builtin/obj/kernel.olean b/src/builtin/obj/kernel.olean
index 6dd8a2e93..898289060 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 5812c0237..815118359 100644
--- a/src/kernel/kernel_decls.cpp
+++ b/src/kernel/kernel_decls.cpp
@@ -22,7 +22,6 @@ 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(em_fn, name("em"));
 MK_CONSTANT(not_intro_fn, name("not_intro"));
 MK_CONSTANT(absurd_fn, name("absurd"));
 MK_CONSTANT(exists_fn, name("exists"));
@@ -33,7 +32,13 @@ MK_CONSTANT(contrapos_fn, name("contrapos"));
 MK_CONSTANT(absurd_elim_fn, name("absurd_elim"));
 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(resolve1_fn, name("resolve1"));
+MK_CONSTANT(resolve2_fn, name("resolve2"));
+MK_CONSTANT(or_flip_fn, name("or_flip"));
+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(subst_fn, name("subst"));
 MK_CONSTANT(substp_fn, name("substp"));
 MK_CONSTANT(symm_fn, name("symm"));
@@ -60,8 +65,9 @@ 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(heqt_elim_fn, name("heqt_elim"));
-MK_CONSTANT(case_fn, name("case"));
 MK_CONSTANT(boolcomplete_fn, name("boolcomplete"));
+MK_CONSTANT(case_fn, name("case"));
+MK_CONSTANT(em_fn, name("em"));
 MK_CONSTANT(boolcomplete_swapped_fn, name("boolcomplete_swapped"));
 MK_CONSTANT(not_true, name("not_true"));
 MK_CONSTANT(not_false, name("not_false"));
@@ -71,15 +77,11 @@ 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(by_contradiction_fn, name("by_contradiction"));
 MK_CONSTANT(boolext_fn, name("boolext"));
 MK_CONSTANT(iff_intro_fn, name("iff_intro"));
 MK_CONSTANT(eqt_intro_fn, name("eqt_intro"));
 MK_CONSTANT(eqf_intro_fn, name("eqf_intro"));
+MK_CONSTANT(by_contradiction_fn, name("by_contradiction"));
 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"));
@@ -96,7 +98,6 @@ 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"));
@@ -112,6 +113,7 @@ 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(or_imp_fn, name("or_imp"));
 MK_CONSTANT(not_congr_fn, name("not_congr"));
 MK_CONSTANT(exists_elim_fn, name("exists_elim"));
 MK_CONSTANT(exists_intro_fn, name("exists_intro"));
@@ -127,20 +129,12 @@ 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"));
-MK_CONSTANT(or_congrr_fn, name("or_congrr"));
-MK_CONSTANT(or_congrl_fn, name("or_congrl"));
-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(and_imp_fn, name("and_imp"));
 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"));
@@ -152,6 +146,15 @@ 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(imp_congrr_fn, name("imp_congrr"));
+MK_CONSTANT(imp_congrl_fn, name("imp_congrl"));
+MK_CONSTANT(imp_congr_fn, name("imp_congr"));
+MK_CONSTANT(or_congrr_fn, name("or_congrr"));
+MK_CONSTANT(or_congrl_fn, name("or_congrl"));
+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(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"));
diff --git a/src/kernel/kernel_decls.h b/src/kernel/kernel_decls.h
index c025a7db6..2a0ca4d21 100644
--- a/src/kernel/kernel_decls.h
+++ b/src/kernel/kernel_decls.h
@@ -55,9 +55,6 @@ 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}); }
@@ -90,9 +87,27 @@ inline expr mk_or_introl_th(expr const & e1, expr const & e2, expr const & 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_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_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_or_flip_fn();
+bool is_or_flip_fn(expr const & e);
+inline expr mk_or_flip_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_or_flip_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_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}); }
@@ -169,12 +184,15 @@ inline expr mk_eqf_elim_th(expr const & e1, expr const & e2) { return mk_app({mk
 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_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_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_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_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_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}); }
@@ -200,21 +218,6 @@ inline expr mk_not_imp_eliml_th(expr const & e1, expr const & e2, expr const & e
 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_by_contradiction_fn();
-bool is_by_contradiction_fn(expr const & e);
-inline expr mk_by_contradiction_th(expr const & e1, expr const & e2) { return mk_app({mk_by_contradiction_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}); }
@@ -227,6 +230,9 @@ inline expr mk_eqt_intro_th(expr const & e1, expr const & e2) { return mk_app({m
 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_by_contradiction_fn();
+bool is_by_contradiction_fn(expr const & e);
+inline expr mk_by_contradiction_th(expr const & e1, expr const & e2) { return mk_app({mk_by_contradiction_fn(), e1, e2}); }
 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}); }
@@ -275,9 +281,6 @@ 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}); }
@@ -323,6 +326,9 @@ 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_or_imp_fn();
+bool is_or_imp_fn(expr const & e);
+inline expr mk_or_imp_th(expr const & e1, expr const & e2) { return mk_app({mk_or_imp_fn(), e1, e2}); }
 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}); }
@@ -369,33 +375,6 @@ inline expr mk_exists_rem_th(expr const & e1, expr const & e2, expr const & 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}); }
-expr mk_imp_congrl_fn();
-bool is_imp_congrl_fn(expr const & e);
-inline expr mk_imp_congrl_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_imp_congrl_fn(), e1, e2, e3, e4, e5, e6}); }
-expr mk_imp_congr_fn();
-bool is_imp_congr_fn(expr const & e);
-inline expr mk_imp_congr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_imp_congr_fn(), e1, e2, e3, e4, e5, e6}); }
-expr mk_or_congrr_fn();
-bool is_or_congrr_fn(expr const & e);
-inline expr mk_or_congrr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_or_congrr_fn(), e1, e2, e3, e4, e5, e6}); }
-expr mk_or_congrl_fn();
-bool is_or_congrl_fn(expr const & e);
-inline expr mk_or_congrl_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_or_congrl_fn(), e1, e2, e3, e4, e5, e6}); }
-expr mk_or_congr_fn();
-bool is_or_congr_fn(expr const & e);
-inline expr mk_or_congr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_or_congr_fn(), e1, e2, e3, e4, e5, e6}); }
-expr mk_and_congrr_fn();
-bool is_and_congrr_fn(expr const & e);
-inline expr mk_and_congrr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_and_congrr_fn(), e1, e2, e3, e4, e5, e6}); }
-expr mk_and_congrl_fn();
-bool is_and_congrl_fn(expr const & e);
-inline expr mk_and_congrl_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_and_congrl_fn(), e1, e2, e3, e4, e5, e6}); }
-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}); }
@@ -411,6 +390,9 @@ inline expr mk_not_or_elim_th(expr const & e1, expr const & e2, expr const & 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_and_imp_fn();
+bool is_and_imp_fn(expr const & e);
+inline expr mk_and_imp_th(expr const & e1, expr const & e2) { return mk_app({mk_and_imp_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}); }
@@ -440,6 +422,33 @@ inline expr mk_not_iff_th(expr const & e1, expr const & e2) { return mk_app({mk_
 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_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}); }
+expr mk_imp_congrl_fn();
+bool is_imp_congrl_fn(expr const & e);
+inline expr mk_imp_congrl_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_imp_congrl_fn(), e1, e2, e3, e4, e5, e6}); }
+expr mk_imp_congr_fn();
+bool is_imp_congr_fn(expr const & e);
+inline expr mk_imp_congr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_imp_congr_fn(), e1, e2, e3, e4, e5, e6}); }
+expr mk_or_congrr_fn();
+bool is_or_congrr_fn(expr const & e);
+inline expr mk_or_congrr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_or_congrr_fn(), e1, e2, e3, e4, e5, e6}); }
+expr mk_or_congrl_fn();
+bool is_or_congrl_fn(expr const & e);
+inline expr mk_or_congrl_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_or_congrl_fn(), e1, e2, e3, e4, e5, e6}); }
+expr mk_or_congr_fn();
+bool is_or_congr_fn(expr const & e);
+inline expr mk_or_congr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_or_congr_fn(), e1, e2, e3, e4, e5, e6}); }
+expr mk_and_congrr_fn();
+bool is_and_congrr_fn(expr const & e);
+inline expr mk_and_congrr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_and_congrr_fn(), e1, e2, e3, e4, e5, e6}); }
+expr mk_and_congrl_fn();
+bool is_and_congrl_fn(expr const & e);
+inline expr mk_and_congrl_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_and_congrl_fn(), e1, e2, e3, e4, e5, e6}); }
+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_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}); }
diff --git a/tests/lean/j5.lean b/tests/lean/j5.lean
index 2c929319f..f8876a89d 100644
--- a/tests/lean/j5.lean
+++ b/tests/lean/j5.lean
@@ -1,3 +1,3 @@
-theorem or_imp (p q : Bool) : (p ∨ q) ↔ (¬ p → q)
+theorem or_imp2 (p q : Bool) : (p ∨ q) ↔ (¬ p → q)
 := subst (symm (imp_or (¬ p) q)) (not_not_eq p)
 
diff --git a/tests/lean/j5.lean.expected.out b/tests/lean/j5.lean.expected.out
index 6ddc0d932..400d4027a 100644
--- a/tests/lean/j5.lean.expected.out
+++ b/tests/lean/j5.lean.expected.out
@@ -1,3 +1,3 @@
   Set: pp::colors
   Set: pp::unicode
-  Proved: or_imp
+  Proved: or_imp2
diff --git a/tests/lean/j6.lean b/tests/lean/j6.lean
index 437a60c80..a6d4e05d9 100644
--- a/tests/lean/j6.lean
+++ b/tests/lean/j6.lean
@@ -1,7 +1,7 @@
 theorem symm_iff (p q : Bool) (H : p ↔ q) : (q ↔ p)
 := symm H
 
-theorem or_imp (p q : Bool) : (p ∨ q) ↔ (¬ p → q)
+theorem or_imp2 (p q : Bool) : (p ∨ q) ↔ (¬ p → q)
 := let H1 := symm_iff _ _ (imp_or (¬ p) q) in
    let H2 := not_not_eq p in
    let H3 := subst H1 H2 in
diff --git a/tests/lean/j6.lean.expected.out b/tests/lean/j6.lean.expected.out
index abe3c1281..8a27e9ede 100644
--- a/tests/lean/j6.lean.expected.out
+++ b/tests/lean/j6.lean.expected.out
@@ -1,4 +1,4 @@
   Set: pp::colors
   Set: pp::unicode
   Proved: symm_iff
-  Proved: or_imp
+  Proved: or_imp2
diff --git a/tests/lean/rs.lean.expected.out b/tests/lean/rs.lean.expected.out
index 8d2d7983a..e17bbb4b2 100644
--- a/tests/lean/rs.lean.expected.out
+++ b/tests/lean/rs.lean.expected.out
@@ -10,7 +10,7 @@ Nat::add_comm : ∀ a b : ℕ, a + b = b + a
 Nat::add_zeror : ∀ a : ℕ, a + 0 = a
 forall_rem [check] : ∀ (A : (Type U)) (H : inhabited A) (p : Bool), (A → p) ↔ p
 eq_id : ∀ (A : (Type U)) (a : A), a = a ↔ ⊤
-exists_rem : ∀ (A : (Type U)) (H : inhabited A) (p : Bool), (∃ x : A, p) ↔ p
+exists_rem : ∀ (A : (Type U)) (H : inhabited A) (p : Bool), (∃ Hb : A, p) ↔ p
 exists_and_distributel : ∀ (A : (Type U)) (p : Bool) (φ : A → Bool),
       (∃ x : A, φ x ∧ p) ↔ (∃ x : A, φ x) ∧ p
 exists_or_distribute : ∀ (A : (Type U)) (φ ψ : A → Bool),