Proofgold Address

Known andE^andE : ∀ x0 x1 : ο . and x0 x1 ⟶ ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Known FalseE^FalseE : False ⟶ ∀ x0 : ο . x0
Known 218d1..^atleast3_E : ∀ x0 . atleast3 x0 ⟶ ∀ x1 : ο . (∀ x2 . and (Subq x2 x0) (and (not (Subq x0 x2)) (atleast2 x2)) ⟶ x1) ⟶ x1
Known notE^notE : ∀ x0 : ο . not x0 ⟶ x0 ⟶ False
Known 39854..^andEL : ∀ x0 x1 : ο . and x0 x1 ⟶ x0
Known b41a2..^Subq_Empty : ∀ x0 . Subq 0 x0
Known 151e5..^exactly3_E : ∀ x0 . exactly3 x0 ⟶ and (atleast3 x0) (not (atleast4 x0))
Theorem 21033.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι . ∀ x2 : ο . (∀ x3 . (∀ x4 . (∃ x5 . and (exactly3 0) (not (x0 x4))) ⟶ ∀ x5 : ο . (∀ x6 . and (and (x0 0) (x0 x4)) (reflexive_i (λ x7 x8 . x0 x7) ⟶ and (x0 x3) (and (x0 (x1 x4)) (not (atleast6 x6)))) ⟶ x5) ⟶ x5) ⟶ x2) ⟶ x2 (proof)
Known 8106d..^notI : ∀ x0 : ο . (x0 ⟶ False) ⟶ not x0
Known 1358f..^nat_TransSet : ∀ x0 . nat_p x0 ⟶ TransSet x0
Known 08405..^nat_0 : nat_p 0
Known b4782..^contra : ∀ x0 : ο . (not x0 ⟶ False) ⟶ x0
Known b0dce..^SubqI : ∀ x0 x1 . (∀ x2 . In x2 x0 ⟶ In x2 x1) ⟶ Subq x0 x1
Theorem 5fbd2.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι . ∀ x2 . (∀ x3 . In x3 x2 ⟶ ∀ x4 . Subq x4 x2 ⟶ and (not (TransSet x4)) (and (and (atleast6 x3) (x0 (x1 x4))) (nat_p (SetAdjoin x2 (binrep (binrep (Power (Power (Power (Power 0)))) (Power 0)) 0))))) ⟶ not (exactly3 x2) (proof)