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 . and (and (∀ x4 . prim1 x4 x0 ⟶ ∃ x5 . and (prim1 x5 x1) (prim1 (7ee77.. x4 x5) x2)) (∀ x4 . prim1 x4 x1 ⟶ ∃ x5 . and (prim1 x5 x0) (prim1 (7ee77.. x5 x4) x2))) (∀ x4 x5 x6 x7 . prim1 (7ee77.. x4 x5) x2 ⟶ prim1 (7ee77.. x6 x7) x2 ⟶ iff (x4 = x6) (x5 = x7))
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 . and (prim1 x1 x2) (prim1 x2 x0))
Axiom 113d7.. : ∀ x0 x1 . prim1 x1 x0 ⟶ ∃ x2 . and (prim1 x2 x0) (not (∃ x4 . and (prim1 x4 x0) (prim1 x4 x2)))
Axiom e8b3c.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 x3 x4 . x1 x2 x3 ⟶ x1 x2 x4 ⟶ x3 = x4) ⟶ ∃ x2 . ∀ x4 . iff (prim1 x4 x2) (∃ x5 . and (prim1 x5 x0) (x1 x5 x4))
Axiom adb47.. : ∀ x0 . ∃ x1 . and (and (and (prim1 x0 x1) (∀ x3 x4 . prim1 x3 x1 ⟶ Subq x4 x3 ⟶ prim1 x4 x1)) (∀ x3 . prim1 x3 x1 ⟶ ∃ x4 . and (prim1 x4 x1) (∀ x6 . Subq x6 x3 ⟶ prim1 x6 x4))) (∀ x3 . Subq x3 x1 ⟶ or (c2e41.. x3 x1) (prim1 x3 x1))