Proofgold Address

Definition or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Theorem bcefe.. : ∀ x0 x1 : ο . or x0 x1 ⟶ ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Definition False^False := ∀ x0 : ο . x0
Definition not := λ x0 : ο . x0 ⟶ False
Param ordinal^ordinal : ι → ο
Param ordsucc^ordsucc : ι → ι
Known neq_0_ordsucc^{neq_0_ordsucc} : ∀ x0 . 0 = ordsucc x0 ⟶ ∀ x1 : ο . x1
Definition nIn^nIn := λ x0 x1 . not (x0 ∈ x1)
Known EmptyE^EmptyE : ∀ x0 . nIn x0 0
Known ordinal_Empty^{ordinal_Empty} : ordinal 0
Known ordinal_ordsucc^{ordinal_ordsucc} : ∀ x0 . ordinal x0 ⟶ ordinal (ordsucc x0)
Theorem 8b4f2.. : not (∀ x0 x1 . ordinal x0 ⟶ ordinal (ordsucc x1) ⟶ or (x0 = ordsucc x1) (ordsucc x1 ∈ x0))