Proofgold Asset

Known 8106d..^notI : ∀ x0 : ο . (x0 ⟶ False) ⟶ not x0
Known e7637..^binrep_E : ∀ x0 x1 x2 . In x2 (binrep x0 x1) ⟶ ∀ x3 : ι → ο . (∀ x4 . In x4 x0 ⟶ x3 (Inj0 x4)) ⟶ (∀ x4 . Subq x4 x1 ⟶ x3 (Inj1 x4)) ⟶ x3 x2
Known 0e45c..^Inj0E : ∀ x0 x1 . In x1 (Inj0 x0) ⟶ ∀ x2 : ο . (∀ x3 . and (In x3 x0) (x1 = Inj1 x3) ⟶ x2) ⟶ x2
Known notE^notE : ∀ x0 : ο . not x0 ⟶ x0 ⟶ False
Known e3ec9..^neq_0_1 : not (0 = 1)
Known 9ae18..^SingE : ∀ x0 x1 . In x1 (Sing x0) ⟶ x1 = x0
Known 8d83e..^Inj1I1 : ∀ x0 . In 0 (Inj1 x0)
Known eb789..^andER : ∀ x0 x1 : ο . and x0 x1 ⟶ x1
Known 1f15b..^SingI : ∀ x0 . In x0 (Sing x0)
Known 24526..^nIn_E2 : ∀ x0 x1 . nIn x0 x1 ⟶ In x0 x1 ⟶ False
Known 18175..^nIn_1_0 : nIn 1 0
Theorem 75c09.. : ∀ x0 : ο . (∀ x1 . (∀ x2 . Subq x2 (binrep (Power (binrep (Power (Power 0)) 0)) (Power 0)) ⟶ ∀ x3 : ο . (∀ x4 . ((∀ x5 . In x5 x1 ⟶ (∀ x6 : ο . (∀ x7 . and (In x7 x2) (not (TransSet x5)) ⟶ x6) ⟶ x6) ⟶ ∀ x6 . In x6 x1 ⟶ ordinal 0) ⟶ ∀ x5 . Subq x5 (Inj0 x4) ⟶ not (In x4 (binrep (Power (binrep (Power (Power 0)) 0)) (Power 0)))) ⟶ x3) ⟶ x3) ⟶ x0) ⟶ x0 (proof)