Proofgold Address

Known df_nfOLD__ax_gen__ax_4__ax_5__df_sb__df_sb_b__ax_6__ax_7__ax_7_b__ax_7_b1__ax_8__ax_8_b__ax_8_b1__ax_9__ax_9_b__ax_9_b1__ax_10__ax_11 : ∀ x0 : ο . ((∀ x1 : ι → ο . wb (wnfOLD x1) (∀ x2 . x1 x2 ⟶ ∀ x3 . x1 x3)) ⟶ (∀ x1 : ι → ο . (∀ x2 . x1 x2) ⟶ ∀ x2 . x1 x2) ⟶ (∀ x1 x2 : ι → ο . (∀ x3 . x1 x3 ⟶ x2 x3) ⟶ (∀ x3 . x1 x3) ⟶ ∀ x3 . x2 x3) ⟶ (∀ x1 : ο . x1 ⟶ ∀ x2 . x1) ⟶ (∀ x1 : ι → ο . ∀ x2 x3 . wb (wsb x1 x2) (wa (wceq (cv x3) (cv x2) ⟶ x1 x3) (wex (λ x4 . wa (wceq (cv x4) (cv x2)) (x1 x4))))) ⟶ (∀ x1 : ι → ο . ∀ x2 . wb (wsb x1 x2) (wa (wceq (cv x2) (cv x2) ⟶ x1 x2) (wex (λ x3 . wa (wceq (cv x3) (cv x3)) (x1 x3))))) ⟶ (∀ x1 . wn (∀ x2 . wn (wceq (cv x2) (cv x1)))) ⟶ (∀ x1 x2 x3 . wceq (cv x1) (cv x2) ⟶ wceq (cv x1) (cv x3) ⟶ wceq (cv x2) (cv x3)) ⟶ (∀ x1 x2 . wceq (cv x1) (cv x2) ⟶ wceq (cv x1) (cv x1) ⟶ wceq (cv x2) (cv x1)) ⟶ (∀ x1 x2 . wceq (cv x1) (cv x2) ⟶ wceq (cv x1) (cv x2) ⟶ wceq (cv x2) (cv x2)) ⟶ (∀ x1 x2 x3 . wceq (cv x1) (cv x2) ⟶ wcel (cv x1) (cv x3) ⟶ wcel (cv x2) (cv x3)) ⟶ (∀ x1 x2 . wceq (cv x1) (cv x2) ⟶ wcel (cv x1) (cv x1) ⟶ wcel (cv x2) (cv x1)) ⟶ (∀ x1 x2 . wceq (cv x1) (cv x2) ⟶ wcel (cv x1) (cv x2) ⟶ wcel (cv x2) (cv x2)) ⟶ (∀ x1 x2 x3 . wceq (cv x1) (cv x2) ⟶ wcel (cv x3) (cv x1) ⟶ wcel (cv x3) (cv x2)) ⟶ (∀ x1 x2 . wceq (cv x1) (cv x2) ⟶ wcel (cv x1) (cv x1) ⟶ wcel (cv x1) (cv x2)) ⟶ (∀ x1 x2 . wceq (cv x1) (cv x2) ⟶ wcel (cv x2) (cv x1) ⟶ wcel (cv x2) (cv x2)) ⟶ (∀ x1 : ι → ο . wn (∀ x2 . x1 x2) ⟶ ∀ x2 . wn (∀ x3 . x1 x3)) ⟶ (∀ x1 : ι → ι → ο . (∀ x2 x3 . x1 x2 x3) ⟶ ∀ x2 x3 . x1 x3 x2) ⟶ x0) ⟶ x0
Theorem df_nfOLD : ∀ x0 : ι → ο . wb (wnfOLD x0) (∀ x1 . x0 x1 ⟶ ∀ x2 . x0 x2) (proof)
Theorem ax_gen : ∀ x0 : ι → ο . (∀ x1 . x0 x1) ⟶ ∀ x1 . x0 x1 (proof)
Theorem ax_4 : ∀ x0 x1 : ι → ο . (∀ x2 . x0 x2 ⟶ x1 x2) ⟶ (∀ x2 . x0 x2) ⟶ ∀ x2 . x1 x2 (proof)
Theorem ax_5 : ∀ x0 : ο . x0 ⟶ ∀ x1 . x0 (proof)
Theorem df_sb : ∀ x0 : ι → ο . ∀ x1 x2 . wb (wsb x0 x1) (wa (wceq (cv x2) (cv x1) ⟶ x0 x2) (wex (λ x3 . wa (wceq (cv x3) (cv x1)) (x0 x3)))) (proof)
Theorem df_sb_b : ∀ x0 : ι → ο . ∀ x1 . wb (wsb x0 x1) (wa (wceq (cv x1) (cv x1) ⟶ x0 x1) (wex (λ x2 . wa (wceq (cv x2) (cv x2)) (x0 x2)))) (proof)
Theorem ax_9d2 : ∀ x0 . wn (∀ x1 . wn (wceq (cv x1) (cv x0))) (proof)
Theorem ax_8d : ∀ x0 x1 x2 . wceq (cv x0) (cv x1) ⟶ wceq (cv x0) (cv x2) ⟶ wceq (cv x1) (cv x2) (proof)
Theorem ax_7_b : ∀ x0 x1 . wceq (cv x0) (cv x1) ⟶ wceq (cv x0) (cv x0) ⟶ wceq (cv x1) (cv x0) (proof)
Theorem ax_7_b1 : ∀ x0 x1 . wceq (cv x0) (cv x1) ⟶ wceq (cv x0) (cv x1) ⟶ wceq (cv x1) (cv x1) (proof)
Theorem ax_8 : ∀ x0 x1 x2 . wceq (cv x0) (cv x1) ⟶ wcel (cv x0) (cv x2) ⟶ wcel (cv x1) (cv x2) (proof)
Theorem ax_8_b : ∀ x0 x1 . wceq (cv x0) (cv x1) ⟶ wcel (cv x0) (cv x0) ⟶ wcel (cv x1) (cv x0) (proof)
Theorem ax_8_b1 : ∀ x0 x1 . wceq (cv x0) (cv x1) ⟶ wcel (cv x0) (cv x1) ⟶ wcel (cv x1) (cv x1) (proof)
Theorem ax_9 : ∀ x0 x1 x2 . wceq (cv x0) (cv x1) ⟶ wcel (cv x2) (cv x0) ⟶ wcel (cv x2) (cv x1) (proof)
Theorem ax_9_b : ∀ x0 x1 . wceq (cv x0) (cv x1) ⟶ wcel (cv x0) (cv x0) ⟶ wcel (cv x0) (cv x1) (proof)
Theorem ax_9_b1 : ∀ x0 x1 . wceq (cv x0) (cv x1) ⟶ wcel (cv x1) (cv x0) ⟶ wcel (cv x1) (cv x1) (proof)
Theorem ax_10 : ∀ x0 : ι → ο . wn (∀ x1 . x0 x1) ⟶ ∀ x1 . wn (∀ x2 . x0 x2) (proof)
Theorem ax_wl_11v : ∀ x0 : ι → ι → ο . (∀ x1 x2 . x0 x1 x2) ⟶ ∀ x1 x2 . x0 x2 x1 (proof)