Proofgold Address

Known eb789..^andER : ∀ x0 x1 : ο . and x0 x1 ⟶ x1
Known False_def^False_def : False = ∀ x1 : ο . x1
Known 22d74..^atleast5_def : atleast5 = λ x1 . ∀ x2 : ο . (∀ x3 . and (Subq x3 x1) (and (not (Subq x1 x3)) (atleast4 x3)) ⟶ x2) ⟶ x2
Known notE^notE : ∀ x0 : ο . not x0 ⟶ x0 ⟶ False
Known 37124..^orE : ∀ x0 x1 : ο . or x0 x1 ⟶ ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Known 9ac15..^xm : ∀ x0 : ο . or x0 (not x0)
Theorem 6e151.. : ∀ x0 . (∀ x1 . nat_p x1) ⟶ ∀ x1 . In x1 x0 ⟶ ∀ x2 : ο . (∀ x3 . ((∀ x4 : ο . (∀ x5 . and (Subq x5 x3) (∃ x6 . and (exactly2 (binrep (Power (Power (Power 0))) 0)) (not (atleast4 (Power 0)))) ⟶ x4) ⟶ x4) ⟶ ∀ x4 . atleast5 (Union 0) ⟶ atleast4 x3) ⟶ x2) ⟶ x2 (proof)