Proofgold Address

Definition False := ∀ x0 : ο . x0
Definition True := ∀ x0 : ο . x0 ⟶ x0
Definition not := λ x0 : ο . x0 ⟶ False
Theorem FalseE : False ⟶ ∀ x0 : ο . x0 (proof)
Theorem TrueI : True (proof)
Theorem notI : ∀ x0 : ο . (x0 ⟶ False) ⟶ not x0 (proof)
Theorem notE : ∀ x0 : ο . not x0 ⟶ x0 ⟶ False (proof)
Definition and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Theorem andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1 (proof)
Theorem andEL : ∀ x0 x1 : ο . and x0 x1 ⟶ x0 (proof)
Theorem andER : ∀ x0 x1 : ο . and x0 x1 ⟶ x1 (proof)
Definition or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Theorem orIL : ∀ x0 x1 : ο . x0 ⟶ or x0 x1 (proof)
Theorem orIR : ∀ x0 x1 : ο . x1 ⟶ or x0 x1 (proof)
Theorem orE : ∀ x0 x1 x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ or x0 x1 ⟶ x2 (proof)
Definition iff := λ x0 x1 : ο . and (x0 ⟶ x1) (x1 ⟶ x0)
Theorem iffEL : ∀ x0 x1 : ο . iff x0 x1 ⟶ x0 ⟶ x1 (proof)
Theorem iffER : ∀ x0 x1 : ο . iff x0 x1 ⟶ x1 ⟶ x0 (proof)
Theorem iffI : ∀ x0 x1 : ο . (x0 ⟶ x1) ⟶ (x1 ⟶ x0) ⟶ iff x0 x1 (proof)
Theorem iff_refl : ∀ x0 : ο . iff x0 x0 (proof)
Known prop_ext_2 : ∀ x0 x1 : ο . (x0 ⟶ x1) ⟶ (x1 ⟶ x0) ⟶ x0 = x1
Theorem pred_ext_2 : ∀ x0 x1 : ι → ο . (∀ x2 . x0 x2 ⟶ x1 x2) ⟶ (∀ x2 . x1 x2 ⟶ x0 x2) ⟶ x0 = x1 (proof)
Theorem pred_ext : ∀ x0 x1 : ι → ο . (∀ x2 . iff (x0 x2) (x1 x2)) ⟶ x0 = x1 (proof)
Definition 8ac9a.. := λ x0 . False
Definition de327.. := λ x0 : ι → ο . λ x1 x2 . or (x0 x2) (x2 = x1)
Theorem 0998e.. : ∀ x0 : ι → ο . ∀ x1 x2 . x0 x2 ⟶ de327.. x0 x1 x2 (proof)
Theorem f147c.. : ∀ x0 : ι → ο . ∀ x1 . de327.. x0 x1 x1 (proof)
Theorem 8bcd6.. : ∀ x0 : ι → ο . ∀ x1 x2 . de327.. x0 x1 x2 ⟶ ∀ x3 : ο . (x0 x2 ⟶ x3) ⟶ (x2 = x1 ⟶ x3) ⟶ x3 (proof)