Proofgold Address

Known Eps_i_ex^Eps_i_R2 : ∀ x0 : ι → ο . (∀ x1 : ο . (∀ x2 . x0 x2 ⟶ x1) ⟶ x1) ⟶ x0 (Eps_i x0)
Known 39854..^andEL : ∀ x0 x1 : ο . and x0 x1 ⟶ x0
Known eb789..^andER : ∀ x0 x1 : ο . and x0 x1 ⟶ x1
Known c1173..^Subq_def : Subq = λ x1 x2 . ∀ x3 . In x3 x1 ⟶ In x3 x2
Known 7f305..^EmptyAx : not (∀ x0 : ο . (∀ x1 . In x1 0 ⟶ x0) ⟶ x0)
Known b4782..^contra : ∀ x0 : ο . (not x0 ⟶ False) ⟶ x0
Known e7295.. : ∀ x0 x1 : ο . x0 = x1 ⟶ and (x0 ⟶ x1) (x1 ⟶ x0)
Known notE^notE : ∀ x0 : ο . not x0 ⟶ x0 ⟶ False
Known 8106d..^notI : ∀ x0 : ο . (x0 ⟶ False) ⟶ not x0
Known fcbcf..^{not_all_ex_demorgan_i} : ∀ x0 : ι → ο . not (∀ x1 . x0 x1) ⟶ ∀ x1 : ο . (∀ x2 . not (x0 x2) ⟶ x1) ⟶ x1
Known 5f823..^{not_ex_all_demorgan_i} : ∀ x0 : ι → ο . not (∀ x1 : ο . (∀ x2 . x0 x2 ⟶ x1) ⟶ x1) ⟶ ∀ x1 . not (x0 x1)
Known 0ff1b.. : ∀ x0 x1 : ο . not (x0 ⟶ x1) ⟶ and x0 (not x1)
Known 91bfe..^dnegI : ∀ x0 : ο . x0 ⟶ not (not x0)
Known 5232a.. : ∀ x0 x1 : ο . (x0 ⟶ x1) ⟶ not x1 ⟶ not x0
Theorem 453a2.. : (∀ x0 . Subq x0 (setsum (Inj0 (SNoLev (binrep (Power (Power (Power 0))) 0))) (Power (Power (Power (Power 0))))) ⟶ ∀ x1 : ο . (∀ x2 . and (In x2 x0) (∀ x3 . ((∀ x4 . (∀ x5 : ο . (∀ x6 . and (Subq x6 x0) (((exactly5 x4 ⟶ not (exactly2 x3)) ⟶ (exactly3 x4 ⟶ not (SNo x4)) ⟶ not (atleast6 x4)) ⟶ not (exactly4 x6)) ⟶ x5) ⟶ x5) ⟶ not (exactly4 x2)) ⟶ atleast2 (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) 0)) ⟶ not (Subq x3 x2)) ⟶ x1) ⟶ x1) ⟶ ∀ x0 : ο . x0 (proof)