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 . and (Subq x2 x1) (and (not (Subq x1 x2)) (atleast4 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 . (∃ x4 . and (Subq x4 x2) (∃ x6 . and (exactly2 (binrep (Power (Power (Power 0))) 0)) (not (atleast4 (Power 0))))) ⟶ ∀ x4 . atleast5 (Union 0) ⟶ atleast4 x2