Proofgold Address

Prim 0/5cb91.. : (ι → ο) → ι
Def False : ο := ∀ x0 : ο . x0
Def not : ο → ο := λ x0 : ο . x0 ⟶ False
Def and : ο → ο → ο := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Def or : ο → ο → ο := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Def iff : ο → ο → ο := λ x0 x1 : ο . and (x0 ⟶ x1) (x1 ⟶ x0)
Axiom prop_ext : ∀ x0 x1 : ο . iff x0 x1 ⟶ x0 = x1
Prim 1/6e234.. : ι → ι → ο
Def Subq : ι → ι → ο := λ x0 x1 . ∀ x2 . prim1 x2 x0 ⟶ prim1 x2 x1
Prim 2/f5912.. : ι → ι → ι
Def 91630.. : ι → ι := λ x0 . prim2 x0 x0
Prim 3/961fc.. : ι → ι
Def 7ee77.. : ι → ι → ι := λ x0 x1 . prim2 (prim2 x0 x1) (91630.. x0)
Def c2e41.. : ι → ι → ο := λ x0 x1 . ∀ x2 : ο . (∀ x3 . and (and (∀ x4 . prim1 x4 x0 ⟶ ∀ x5 : ο . (∀ x6 . and (prim1 x6 x1) (prim1 (7ee77.. x4 x6) x3) ⟶ x5) ⟶ x5) (∀ x4 . prim1 x4 x1 ⟶ ∀ x5 : ο . (∀ x6 . and (prim1 x6 x0) (prim1 (7ee77.. x6 x4) x3) ⟶ x5) ⟶ x5)) (∀ x4 x5 x6 x7 . prim1 (7ee77.. x4 x5) x3 ⟶ prim1 (7ee77.. x6 x7) x3 ⟶ iff (x4 = x6) (x5 = x7)) ⟶ x2) ⟶ x2
Axiom Eps_i_ax : ∀ x0 : ι → ο . ∀ x1 . x0 x1 ⟶ x0 (prim0 x0)
Axiom 0ddd1.. : ∀ x0 x1 . (∀ x2 . iff (prim1 x2 x0) (prim1 x2 x1)) ⟶ x0 = x1
Axiom 53c21.. : ∀ x0 x1 x2 . iff (prim1 x0 (prim2 x1 x2)) (or (x0 = x1) (x0 = x2))
Axiom UnionEq : ∀ x0 x1 . iff (prim1 x1 (prim3 x0)) (∀ x2 : ο . (∀ x3 . and (prim1 x1 x3) (prim1 x3 x0) ⟶ x2) ⟶ x2)
Axiom 113d7.. : ∀ x0 x1 . prim1 x1 x0 ⟶ ∀ x2 : ο . (∀ x3 . and (prim1 x3 x0) (not (∀ x4 : ο . (∀ x5 . and (prim1 x5 x0) (prim1 x5 x3) ⟶ x4) ⟶ x4)) ⟶ x2) ⟶ x2
Axiom e8b3c.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 x3 x4 . x1 x2 x3 ⟶ x1 x2 x4 ⟶ x3 = x4) ⟶ ∀ x2 : ο . (∀ x3 . (∀ x4 . iff (prim1 x4 x3) (∀ x5 : ο . (∀ x6 . and (prim1 x6 x0) (x1 x6 x4) ⟶ x5) ⟶ x5)) ⟶ x2) ⟶ x2
Axiom adb47.. : ∀ x0 . ∀ x1 : ο . (∀ x2 . and (and (and (prim1 x0 x2) (∀ x3 x4 . prim1 x3 x2 ⟶ Subq x4 x3 ⟶ prim1 x4 x2)) (∀ x3 . prim1 x3 x2 ⟶ ∀ x4 : ο . (∀ x5 . and (prim1 x5 x2) (∀ x6 . Subq x6 x3 ⟶ prim1 x6 x5) ⟶ x4) ⟶ x4)) (∀ x3 . Subq x3 x2 ⟶ or (c2e41.. x3 x2) (prim1 x3 x2)) ⟶ x1) ⟶ x1