Theory bool

[oracles: ] [axioms: BOOL_CASES_AX] [] ⊢ ∀t. (t ⇔ T) ∨ (t ⇔ F)

[oracles: ] [axioms: ETA_AX] [] ⊢ ∀t. (λx. t x) = t

[oracles: ] [axioms: INFINITY_AX] [] ⊢ ∃f. ONE_ONE f ∧ ¬ONTO f

[oracles: ] [axioms: SELECT_AX] [] ⊢ ∀P x. P x ⇒ P ($@ P)

⊢ $/\ = (λt1 t2. ∀t. (t1 ⇒ t2 ⇒ t) ⇒ t)

⊢ BOUNDED = (λv. T)

⊢ COND = (λt t1 t2. @x. ((t ⇔ T) ⇒ x = t1) ∧ ((t ⇔ F) ⇒ x = t2))

⊢ DATATYPE = (λx. T)

⊢ $? = (λP. P ($@ P))

⊢ $?! = (λP. $? P ∧ ∀x y. P x ∧ P y ⇒ x = y)

⊢ $! = (λP. P = (λx. T))

⊢ F ⇔ ∀t. t

⊢ $IN = (λx f. f x)

⊢ LET = (λf x. f x)

⊢ $¬ = (λt. t ⇒ F)

⊢ ONE_ONE = (λf. ∀x1 x2. f x1 = f x2 ⇒ x1 = x2)

⊢ ONTO = (λf. ∀y. ∃x. y = f x)

⊢ $\/ = (λt1 t2. ∀t. (t1 ⇒ t) ⇒ (t2 ⇒ t) ⇒ t)

[oracles: ] [axioms: ETA_AX, BOOL_CASES_AX, SELECT_AX] []
⊢ (∀p m x. x ∈ p ⇒ RES_ABSTRACT p m x = m x) ∧
  ∀p m1 m2.
    (∀x. x ∈ p ⇒ m1 x = m2 x) ⇒ RES_ABSTRACT p m1 = RES_ABSTRACT p m2

⊢ RES_EXISTS = (λp m. ∃x. x ∈ p ∧ m x)

⊢ RES_EXISTS_UNIQUE = (λp m. (∃x::p. m x) ∧ ∀x y::p. m x ∧ m y ⇒ x = y)

⊢ RES_FORALL = (λp m. ∀x. x ∈ p ⇒ m x)

⊢ RES_SELECT = (λp m. @x. x ∈ p ∧ m x)

⊢ TYPE_DEFINITION =
  (λP rep.
       (∀x' x''. rep x' = rep x'' ⇒ x' = x'') ∧ ∀x. P x ⇔ ∃x'. x = rep x')

⊢ T ⇔ (λx. x) = (λx. x)

[oracles: ] [axioms: BOOL_CASES_AX] [] ⊢ ∃rep. TYPE_DEFINITION ($= ARB) rep

⊢ ∀b. itself_case (:α) b = b

⊢ literal_case = (λf x. f x)

[oracles: ] [axioms: BOOL_CASES_AX, SELECT_AX] []
⊢ ∀P. (∃rep. TYPE_DEFINITION P rep) ⇒
      ∃rep abs. (∀a. abs (rep a) = a) ∧ ∀r. P r ⇔ rep (abs r) = r

⊢ ∀t1 t2. (λx. t1) t2 = t1

⊢ ∀t1 t2. t1 ∧ t2 ⇒ t1

⊢ ∀t1 t2. t1 ∧ t2 ⇒ t2

[oracles: ] [axioms: BOOL_CASES_AX] []
⊢ ∀t. (T ∧ t ⇔ t) ∧ (t ∧ T ⇔ t) ∧ (F ∧ t ⇔ F) ∧ (t ∧ F ⇔ F) ∧ (t ∧ t ⇔ t)

[oracles: ] [axioms: BOOL_CASES_AX] []
⊢ ∀P P' Q Q'. (Q ⇒ (P ⇔ P')) ∧ (P' ⇒ (Q ⇔ Q')) ⇒ (P ∧ Q ⇔ P' ∧ Q')

[oracles: ] [axioms: BOOL_CASES_AX] []
⊢ ∀t1 t2 t3. t1 ⇒ t2 ⇒ t3 ⇔ t1 ∧ t2 ⇒ t3

⊢ ∀t1 t2. t1 ⇒ t2 ⇒ t1 ∧ t2

⊢ ∀f y. (λx. f x) y = f y

⊢ (T ⇎ F) ∧ (F ⇎ T)

[oracles: ] [axioms: BOOL_CASES_AX, ETA_AX] []
⊢ ∀f. f = (λb. T) ∨ f = (λb. F) ∨ f = (λb. b) ∨ f = (λb. ¬b)

[oracles: ] [axioms: ETA_AX, BOOL_CASES_AX] []
⊢ ∀P. P (λb. T) ∧ P (λb. F) ∧ P (λb. b) ∧ P (λb. ¬b) ⇒ ∀f. P f

[oracles: ] [axioms: BOOL_CASES_AX] []
⊢ ∀P Q. (∃x. P ∧ Q) ⇔ (∃x. P) ∧ ∃x. Q

[oracles: ] [axioms: BOOL_CASES_AX] []
⊢ ∀P Q. (∃x. P ⇒ Q) ⇔ (∀x. P) ⇒ ∃x. Q

[oracles: ] [axioms: BOOL_CASES_AX] []
⊢ ∀P Q. (∀x. P ⇒ Q) ⇔ (∃x. P) ⇒ ∀x. Q

[oracles: ] [axioms: BOOL_CASES_AX] []
⊢ ∀P Q. (∀x. P ∨ Q) ⇔ (∀x. P) ∨ ∀x. Q

⊢ ∀v. BOUNDED v ⇔ T

[oracles: ] [axioms: SELECT_AX, BOOL_CASES_AX, ETA_AX] []
⊢ ∀b f g. (λx. if b then f x else g x) = if b then f else g

[oracles: ] [axioms: BOOL_CASES_AX, SELECT_AX] []
⊢ ∀t1 t2. (if T then t1 else t2) = t1 ∧ (if F then t1 else t2) = t2

[oracles: ] [axioms: BOOL_CASES_AX, SELECT_AX] []
⊢ ∀P Q x x' y y'.
    (P ⇔ Q) ∧ (Q ⇒ x = x') ∧ (¬Q ⇒ y = y') ⇒
    (if P then x else y) = if Q then x' else y'

[oracles: ] [axioms: SELECT_AX, BOOL_CASES_AX] []
⊢ ∀b t1 t2. (if b then t1 else t2) ⇔ (¬b ∨ t1) ∧ (b ∨ t2)

[oracles: ] [axioms: SELECT_AX, BOOL_CASES_AX] []
⊢ ∀b t1 t2. (if b then t1 else t2) ⇔ (b ⇒ t1) ∧ (¬b ⇒ t2)

[oracles: ] [axioms: SELECT_AX, BOOL_CASES_AX] []
⊢ ∀b t1 t2. (if b then t1 else t2) ⇔ b ∧ t1 ∨ ¬b ∧ t2

[oracles: ] [axioms: BOOL_CASES_AX, SELECT_AX] []
⊢ ∀b t. (if b then t else t) = t

[oracles: ] [axioms: BOOL_CASES_AX, SELECT_AX] []
⊢ ∀f b x y. f (if b then x else y) = if b then f x else f y

[oracles: ] [axioms: BOOL_CASES_AX, SELECT_AX] []
⊢ ∀b f g x. (if b then f else g) x = if b then f x else g x

[oracles: ] [axioms: BOOL_CASES_AX] []
⊢ ∀t1 t2 t3. t1 ∧ t2 ∧ t3 ⇔ (t1 ∧ t2) ∧ t3

[oracles: ] [axioms: BOOL_CASES_AX] [] ⊢ ∀t1 t2. t1 ∧ t2 ⇔ t2 ∧ t1

[oracles: ] [axioms: BOOL_CASES_AX] [] ⊢ ∀t1 t2. t1 ∧ t2 ⇔ t2 ∧ t1

[oracles: ] [axioms: BOOL_CASES_AX] [] ⊢ ∀t1 t2. ¬t1 ⇒ ¬t2 ⇔ t2 ⇒ t1

⊢ DATATYPE (bool T F) ⇔ T

⊢ ∀x. DATATYPE x ⇔ T

[oracles: ] [axioms: BOOL_CASES_AX] []
⊢ ∀A B. (¬(A ∧ B) ⇔ ¬A ∨ ¬B) ∧ (¬(A ∨ B) ⇔ ¬A ∧ ¬B)

[oracles: ] [axioms: BOOL_CASES_AX] [] ⊢ ∀A B C. A ∨ B ∨ C ⇔ (A ∨ B) ∨ C

[oracles: ] [axioms: BOOL_CASES_AX] [] ⊢ ∀A B. A ∨ B ⇔ B ∨ A

[oracles: ] [axioms: BOOL_CASES_AX] [] ⊢ ∀A B. A ∨ B ⇔ ¬A ⇒ B

[oracles: ] [axioms: BOOL_CASES_AX] []
⊢ ∀P Q R. P ∨ Q ⇒ R ⇔ (P ⇒ R) ∧ (Q ⇒ R)

[oracles: ] [axioms: BOOL_CASES_AX] [] ⊢ ∀A B. A ∨ B ⇔ B ∨ A

[oracles: ] [axioms: BOOL_CASES_AX] []
⊢ ∀t. ((T ⇔ t) ⇔ t) ∧ ((t ⇔ T) ⇔ t) ∧ ((F ⇔ t) ⇔ ¬t) ∧ ((t ⇔ F) ⇔ ¬t)

[oracles: ] [axioms: BOOL_CASES_AX] []
⊢ ∀t1 t2. (t1 ⇔ t2) ⇔ t1 ∧ t2 ∨ ¬t1 ∧ ¬t2

[oracles: ] [axioms: ETA_AX] [] ⊢ ∀f g. (∀x. f x = g x) ⇒ f = g

[oracles: ] [axioms: BOOL_CASES_AX] [] ⊢ ∀t1 t2. (t1 ⇔ t2) ⇒ t1 ⇒ t2

[oracles: ] [axioms: BOOL_CASES_AX] []
⊢ ∀t1 t2. (t1 ⇔ t2) ⇔ (t1 ⇒ t2) ∧ (t2 ⇒ t1)

⊢ ∀x. x = x

⊢ ∀x y. x = y ⇒ y = x

[oracles: ] [axioms: BOOL_CASES_AX] [] ⊢ ∀x y. x = y ⇔ y = x

⊢ ∀x y z. x = y ∧ y = z ⇒ x = z

[oracles: ] [axioms: ETA_AX] [] ⊢ ∀M. (λx. M x) = M

[oracles: ] [axioms: BOOL_CASES_AX] [] ⊢ ∀t. t ∨ ¬t

[oracles: ] [axioms: BOOL_CASES_AX] []
⊢ ∀P Q. (∃x. P x ∨ Q x) ⇔ (∃x. P x) ∨ ∃x. Q x

⊢ ∀a. ∃x. x = a

[oracles: ] [axioms: BOOL_CASES_AX] [] ⊢ ∀t. (∃x. t) ⇔ t

[oracles: ] [axioms: ETA_AX] [] ⊢ $? f ⇔ ∃x. f x

[oracles: ] [axioms: BOOL_CASES_AX] [] ⊢ (∃!x. P x) ⇔ ∃x. ∀y. P y ⇔ y = x

[oracles: ] [axioms: BOOL_CASES_AX] [] ⊢ (∃!x. F) ⇔ F

⊢ ∀a. ∃!x. x = a

⊢ (∃!x. P x) ⇔ (∃x. P x) ∧ ∀x y. P x ∧ P y ⇒ x = y

[oracles: ] [axioms: BOOL_CASES_AX] [] ⊢ (∃x. P x) ⇔ P (:α)

⊢ ∀t. F ⇒ t

[oracles: ] [axioms: BOOL_CASES_AX] []
⊢ ∀P Q. (∀x. P x ∧ Q x) ⇔ (∀x. P x) ∧ ∀x. Q x

[oracles: ] [axioms: BOOL_CASES_AX] [] ⊢ (∀b. P b) ⇔ P T ∧ P F

[oracles: ] [axioms: BOOL_CASES_AX] [] ⊢ ∀t. (∀x. t) ⇔ t

[oracles: ] [axioms: ETA_AX] [] ⊢ $! f ⇔ ∀x. f x

[oracles: ] [axioms: BOOL_CASES_AX] [] ⊢ (∀x. P x) ⇔ P (:α)

[oracles: ] [axioms: BOOL_CASES_AX, ETA_AX] []
⊢ ∀f g. f = g ⇔ ∀x. f x = g x

⊢ ∀t. ¬t ⇒ t ⇒ F

[oracles: ] [axioms: BOOL_CASES_AX] []
⊢ ∀t1 t2. (t1 ⇒ t2) ⇒ (t2 ⇒ t1) ⇒ (t1 ⇔ t2)

[oracles: ] [axioms: BOOL_CASES_AX] []
⊢ ∀t. (T ⇒ t ⇔ t) ∧ (t ⇒ T ⇔ T) ∧ (F ⇒ t ⇔ T) ∧ (t ⇒ t ⇔ T) ∧ (t ⇒ F ⇔ ¬t)

[oracles: ] [axioms: BOOL_CASES_AX] []
⊢ ∀x x' y y'. (x ⇔ x') ∧ (x' ⇒ (y ⇔ y')) ⇒ (x ⇒ y ⇔ x' ⇒ y')

[oracles: ] [axioms: BOOL_CASES_AX] []
⊢ ∀P Q R. P ⇒ Q ∧ R ⇔ (P ⇒ Q) ∧ (P ⇒ R)

[oracles: ] [axioms: BOOL_CASES_AX] [] ⊢ ∀A B. A ⇒ B ⇔ ¬A ∨ B

⊢ ∀t. (t ⇒ F) ⇒ ¬t

[oracles: ] [axioms: BOOL_CASES_AX] [] ⊢ ∀t. t ⇒ F ⇔ (t ⇔ F)

[oracles: ] [axioms: BOOL_CASES_AX] [] ⊢ ∀f e. f (:α) = e ⇔ ∀x. f x = e

[oracles: ] [axioms: BOOL_CASES_AX] [] ⊢ ∀i. i = (:α)

[oracles: ] [axioms: ETA_AX] [] ⊢ ∀P t. (∀x. x = t ⇒ P x) ⇒ $? P

⊢ ∀f. (∀x y z. f x (f y z) = f (f x y) z) ⇒
      (∀x y. f x y = f y x) ⇒
      ∀x y z. f x (f y z) = f y (f x z)

[oracles: ] [axioms: BOOL_CASES_AX] []
⊢ ∀P P' Q Q'. (P ⇔ P') ∧ (P' ⇒ (Q ⇔ Q')) ⇒ (P ∧ Q ⇔ P' ∧ Q')

[oracles: ] [axioms: BOOL_CASES_AX] [] ⊢ ∀P Q. (∀x. P x) ∧ Q ⇔ ∀x. P x ∧ Q

[oracles: ] [axioms: BOOL_CASES_AX] []
⊢ ∀A B C. A ∧ (B ∨ C) ⇔ A ∧ B ∨ A ∧ C

[oracles: ] [axioms: BOOL_CASES_AX] []
⊢ ∀P Q. (∃x. P x ∧ Q) ⇔ (∃x. P x) ∧ Q

[oracles: ] [axioms: BOOL_CASES_AX] []
⊢ ∀P Q. (∃x. P x ⇒ Q) ⇔ (∀x. P x) ⇒ Q

[oracles: ] [axioms: BOOL_CASES_AX] []
⊢ ∀P Q. (∀x. P x ⇒ Q) ⇔ (∃x. P x) ⇒ Q

[oracles: ] [axioms: BOOL_CASES_AX] []
⊢ ∀P Q. (∀x. P x ∨ Q) ⇔ (∀x. P x) ∨ Q

[oracles: ] [axioms: BOOL_CASES_AX] []
⊢ ∀P P' Q Q'. (P ⇔ P') ∧ (¬P' ⇒ (Q ⇔ Q')) ⇒ (P ∨ Q ⇔ P' ∨ Q')

[oracles: ] [axioms: BOOL_CASES_AX] [] ⊢ ∀P Q. (∃x. P x) ∨ Q ⇔ ∃x. P x ∨ Q

[oracles: ] [axioms: BOOL_CASES_AX] []
⊢ ∀A B C. A ∨ B ∧ C ⇔ (A ∨ B) ∧ (A ∨ C)

[oracles: ] [axioms: BOOL_CASES_AX] []
⊢ ∀f g M N. M = N ∧ (∀x. x = N ⇒ f x = g x) ⇒ LET f M = LET g N

⊢ P (let x = M in N x) ⇔ (let x = M in P (N x))

⊢ (let x = M in N x) b = (let x = M in N x b)

⊢ ∀f x. LET f x = f x

⊢ (∀x. P x ⇒ Q x) ⇒ (∀x. P x) ⇒ ∀x. Q x

[oracles: ] [axioms: BOOL_CASES_AX] [] ⊢ (x ⇒ y) ∧ (z ⇒ w) ⇒ x ∧ z ⇒ y ∧ w

[oracles: ] [axioms: BOOL_CASES_AX, SELECT_AX] []
⊢ (x ⇒ y) ⇒ (z ⇒ w) ⇒ (if b then x else z) ⇒ if b then y else w

⊢ (∀x. P x ⇒ Q x) ⇒ (∃x. P x) ⇒ ∃x. Q x

[oracles: ] [axioms: BOOL_CASES_AX] []
⊢ (y ⇒ x) ∧ (z ⇒ w) ⇒ (x ⇒ z) ⇒ y ⇒ w

⊢ (y ⇒ x) ⇒ ¬x ⇒ ¬y

[oracles: ] [axioms: BOOL_CASES_AX] [] ⊢ y ⇒ x ⇔ ¬x ⇒ ¬y

[oracles: ] [axioms: BOOL_CASES_AX] [] ⊢ (x ⇒ y) ∧ (z ⇒ w) ⇒ x ∨ z ⇒ y ∨ w

⊢ ¬(t ∧ ¬t)

[oracles: ] [axioms: BOOL_CASES_AX] []
⊢ (∀t. ¬¬t ⇔ t) ∧ (¬T ⇔ F) ∧ (¬F ⇔ T)

[oracles: ] [axioms: BOOL_CASES_AX] [] ⊢ ∀P. ¬(∃x. P x) ⇔ ∀x. ¬P x

[oracles: ] [axioms: BOOL_CASES_AX] [] ⊢ ∀t. ¬t ⇒ (t ⇔ F)

[oracles: ] [axioms: BOOL_CASES_AX] [] ⊢ ∀P. ¬(∀x. P x) ⇔ ∃x. ¬P x

[oracles: ] [axioms: BOOL_CASES_AX] [] ⊢ ∀A B. ¬(A ⇒ B) ⇔ A ∧ ¬B

⊢ ∀f. ONE_ONE f ⇔ ∀x1 x2. f x1 = f x2 ⇒ x1 = x2

⊢ ∀f. ONTO f ⇔ ∀y. ∃x. y = f x

[oracles: ] [axioms: BOOL_CASES_AX] []
⊢ ∀t. (T ∨ t ⇔ T) ∧ (t ∨ T ⇔ T) ∧ (F ∨ t ⇔ t) ∧ (t ∨ F ⇔ t) ∧ (t ∨ t ⇔ t)

[oracles: ] [axioms: BOOL_CASES_AX] []
⊢ ∀P P' Q Q'. (¬Q ⇒ (P ⇔ P')) ∧ (¬P' ⇒ (Q ⇔ Q')) ⇒ (P ∨ Q ⇔ P' ∨ Q')

⊢ ∀t t1 t2. t1 ∨ t2 ⇒ (t1 ⇒ t) ⇒ (t2 ⇒ t) ⇒ t

[oracles: ] [axioms: BOOL_CASES_AX] [] ⊢ ∀A B. (A ⇔ B ∨ A) ⇔ B ⇒ A

⊢ ∀t1 t2. t1 ⇒ t1 ∨ t2

⊢ ∀t1 t2. t2 ⇒ t1 ∨ t2

[oracles: ] [axioms: BOOL_CASES_AX] [] ⊢ ((P ⇒ Q) ⇒ P) ⇒ P

[oracles: ] [axioms: BOOL_CASES_AX] []
⊢ ∀P Q.
    ((∃x. P x) ⇒ Q ⇔ ∀x. P x ⇒ Q) ∧ ((∃x. P x) ∧ Q ⇔ ∃x. P x ∧ Q) ∧
    (Q ∧ (∃x. P x) ⇔ ∃x. Q ∧ P x)

[oracles: ] [axioms: BOOL_CASES_AX] []
⊢ ∀P Q.
    (Q ⇒ (∀x. P x) ⇔ ∀x. Q ⇒ P x) ∧ ((∀x. P x) ∧ Q ⇔ ∀x. P x ∧ Q) ∧
    (Q ∧ (∀x. P x) ⇔ ∀x. Q ∧ P x)

[oracles: ] [axioms: BOOL_CASES_AX] [] ⊢ ∀x. x = x ⇔ T

[oracles: ] [axioms: BOOL_CASES_AX] []
⊢ P = Q ⇒ (∀x. x ∈ Q ⇒ (f x ⇔ g x)) ⇒ (RES_EXISTS P f ⇔ RES_EXISTS Q g)

[oracles: ] [axioms: BOOL_CASES_AX] [] ⊢ (∃x::P. F) ⇔ F

⊢ ∀P f. RES_EXISTS P f ⇔ ∃x. x ∈ P ∧ f x

⊢ ∀P f. RES_EXISTS_UNIQUE P f ⇔ (∃x::P. f x) ∧ ∀x y::P. f x ∧ f y ⇒ x = y

[oracles: ] [axioms: BOOL_CASES_AX] []
⊢ P = Q ⇒ (∀x. x ∈ Q ⇒ (f x ⇔ g x)) ⇒ (RES_FORALL P f ⇔ RES_FORALL Q g)

⊢ ∀P f. RES_FORALL P f ⇔ ∀x. x ∈ P ⇒ f x

[oracles: ] [axioms: BOOL_CASES_AX] [] ⊢ (∀x::P. T) ⇔ T

⊢ ∀P f. RES_SELECT P f = @x. x ∈ P ∧ f x

[oracles: ] [axioms: BOOL_CASES_AX] [] ⊢ ∀P Q. P ∧ (∀x. Q x) ⇔ ∀x. P ∧ Q x

[oracles: ] [axioms: BOOL_CASES_AX] []
⊢ ∀A B C. (B ∨ C) ∧ A ⇔ B ∧ A ∨ C ∧ A

[oracles: ] [axioms: BOOL_CASES_AX] [] ⊢ ∀P Q. (∃x. P ∧ Q x) ⇔ P ∧ ∃x. Q x

[oracles: ] [axioms: BOOL_CASES_AX] [] ⊢ ∀P Q. (∃x. P ⇒ Q x) ⇔ P ⇒ ∃x. Q x

[oracles: ] [axioms: BOOL_CASES_AX] [] ⊢ ∀P Q. (∀x. P ⇒ Q x) ⇔ P ⇒ ∀x. Q x

[oracles: ] [axioms: BOOL_CASES_AX] [] ⊢ ∀P Q. (∀x. P ∨ Q x) ⇔ P ∨ ∀x. Q x

[oracles: ] [axioms: BOOL_CASES_AX] [] ⊢ ∀P Q. P ∨ (∃x. Q x) ⇔ ∃x. P ∨ Q x

[oracles: ] [axioms: BOOL_CASES_AX] []
⊢ ∀A B C. B ∧ C ∨ A ⇔ (B ∨ A) ∧ (C ∨ A)

[oracles: ] [axioms: SELECT_AX] []
⊢ ∀P Q. (∃x. P x) ∧ (∀x. P x ⇒ Q x) ⇒ Q ($@ P)

[oracles: ] [axioms: SELECT_AX] [] ⊢ ∀x. (@y. y = x) = x

[oracles: ] [axioms: SELECT_AX] [] ⊢ ∀x. (@y. x = y) = x

⊢ ∀P. P (@x. P x) ⇔ ∃x. P x

[oracles: ] [axioms: ETA_AX, BOOL_CASES_AX, SELECT_AX] []
⊢ ∀P x. (∀y. P y ⇔ y = x) ⇒ $@ P = x

[oracles: ] [axioms: BOOL_CASES_AX, SELECT_AX] []
⊢ ∀P. (∀x. ∃y. P x y) ⇔ ∃f. ∀x. P x (f x)

[oracles: ] [axioms: BOOL_CASES_AX] [] ⊢ ∀P. (∃x y. P x y) ⇔ ∃y x. P x y

[oracles: ] [axioms: BOOL_CASES_AX] [] ⊢ ∀P. (∀x y. P x y) ⇔ ∀y x. P x y

⊢ T

⊢ ∀P rep.
    TYPE_DEFINITION P rep ⇔
    (∀x' x''. rep x' = rep x'' ⇒ x' = x'') ∧ ∀x. P x ⇔ ∃x'. x = rep x'

[oracles: ] [axioms: BOOL_CASES_AX] []
⊢ ∀P Q. (∃!x. P x ∨ Q x) ⇒ (∃!x. P x) ∨ ∃!x. Q x

[oracles: ] [axioms: BOOL_CASES_AX] [] ⊢ (∃!x. t) ⇔ t ∧ ∀x y. x = y

[oracles: ] [axioms: BOOL_CASES_AX] [] ⊢ ∀f v. (∀x. v = x ⇒ f x) ⇔ f v

[oracles: ] [axioms: BOOL_CASES_AX] [] ⊢ ∀f v. (∀x. x = v ⇒ f x) ⇔ f v

[oracles: ] [axioms: BOOL_CASES_AX] [] ⊢ ∀P a. (∃x. a = x ∧ P x) ⇔ P a

[oracles: ] [axioms: BOOL_CASES_AX] [] ⊢ ∀P a. (∃x. x = a ∧ P x) ⇔ P a

[oracles: ] [axioms: BOOL_CASES_AX, SELECT_AX] []
⊢ ∀t1 t2. ∃fn. fn T = t1 ∧ fn F = t2

[oracles: ] [axioms: BOOL_CASES_AX] [] ⊢ ∀P. P T ∧ P F ⇒ ∀b. P b

[oracles: ] [axioms: BOOL_CASES_AX, SELECT_AX] []
⊢ ∀P Q x x' y y'.
    (P ⇔ Q) ∧ (Q ⇒ x = x') ∧ (¬Q ⇒ y = y') ⇒
    (if P then x else y) = if Q then x' else y'

[oracles: ] [axioms: BOOL_CASES_AX, SELECT_AX] []
⊢ ∀b t. (if b then t else t) = t

[oracles: ] [axioms: BOOL_CASES_AX, SELECT_AX] []
⊢ ∀x. (if x then T else F) ⇔ x

[oracles: ] [axioms: SELECT_AX, BOOL_CASES_AX] []
⊢ (if x then t1 else t2) = v ⇔ (x ⇔ T) ∧ t1 = v ∨ (x ⇔ F) ∧ t2 = v

[oracles: ] [axioms: BOOL_CASES_AX, SELECT_AX] []
⊢ (∀t1 t2. (if T then t1 else t2) = t1) ∧
  ∀t1 t2. (if F then t1 else t2) = t2

⊢ ∀e. ∃f. f (:α) = e

[oracles: ] [axioms: BOOL_CASES_AX] [] ⊢ ∀P. P (:α) ⇒ ∀i. P i

[oracles: ] [axioms: BOOL_CASES_AX] []
⊢ ∀f g M N.
    M = N ∧ (∀x. x = N ⇒ f x = g x) ⇒ literal_case f M = literal_case g N

⊢ P (literal_case (λx. N x) M) = literal_case (λx. P (N x)) M

⊢ literal_case (λx. N x) M b = literal_case (λx. N x b) M

⊢ ∀f x. literal_case f x = f x

[oracles: ] [axioms: BOOL_CASES_AX, SELECT_AX] []
⊢ literal_case (λx. if x = a then t else u) a = t