Apply 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 with ∀ x0 x1 . wceq (cv x0) (cv x1) ⟶ wceq (cv x0) (cv x1) ⟶ wceq (cv x1) (cv x1).

Assume H0: ∀ x0 : ι → ο . wb (wnfOLD (λ x1 . x0 x1)) (∀ x1 . x0 x1 ⟶ ∀ x2 . x0 x2).

Assume H1: ∀ x0 : ι → ο . (∀ x1 . x0 x1) ⟶ ∀ x1 . x0 x1.

Assume H2: ∀ x0 x1 : ι → ο . (∀ x2 . x0 x2 ⟶ x1 x2) ⟶ (∀ x2 . x0 x2) ⟶ ∀ x2 . x1 x2.

Assume H3: ∀ x0 : ο . x0 ⟶ ∀ x1 . x0.

Assume H4: ∀ x0 : ι → ο . ∀ x1 x2 . wb (wsb (λ x3 . x0 x3) x1) (wa (wceq (cv x2) (cv x1) ⟶ x0 x2) (wex (λ x3 . wa (wceq (cv x3) (cv x1)) (x0 x3)))).

Assume H5: ∀ x0 : ι → ο . ∀ x1 . wb (wsb (λ x2 . x0 x2) x1) (wa (wceq (cv x1) (cv x1) ⟶ x0 x1) (wex (λ x2 . wa (wceq (cv x2) (cv x2)) (x0 x2)))).

Assume H6: ∀ x0 . wn (∀ x1 . wn (wceq (cv x1) (cv x0))).

Assume H7: ∀ x0 x1 x2 . wceq (cv x0) (cv x1) ⟶ wceq (cv x0) (cv x2) ⟶ wceq (cv x1) (cv x2).

Assume H8: ∀ x0 x1 . wceq (cv x0) (cv x1) ⟶ wceq (cv x0) (cv x0) ⟶ wceq (cv x1) (cv x0).

Assume H9: ∀ x0 x1 . wceq (cv x0) (cv x1) ⟶ wceq (cv x0) (cv x1) ⟶ wceq (cv x1) (cv x1).

Assume H10: ∀ x0 x1 x2 . wceq (cv x0) (cv x1) ⟶ wcel (cv x0) (cv x2) ⟶ wcel (cv x1) (cv x2).

Assume H11: ∀ x0 x1 . wceq (cv x0) (cv x1) ⟶ wcel (cv x0) (cv x0) ⟶ wcel (cv x1) (cv x0).

Assume H12: ∀ x0 x1 . wceq (cv x0) (cv x1) ⟶ wcel (cv x0) (cv x1) ⟶ wcel (cv x1) (cv x1).

Assume H13: ∀ x0 x1 x2 . wceq (cv x0) (cv x1) ⟶ wcel (cv x2) (cv x0) ⟶ wcel (cv x2) (cv x1).

Assume H14: ∀ x0 x1 . wceq (cv x0) (cv x1) ⟶ wcel (cv x0) (cv x0) ⟶ wcel (cv x0) (cv x1).

Assume H15: ∀ x0 x1 . ... ⟶ ... ⟶ wcel (cv ...) ....

...

■

Proofgold Proof