Apply ax_c11__ax_c11_b__ax_c11n__ax_c15__ax_c9__ax_c9_b__ax_c9_b1__ax_c9_b2__ax_c9_b3__ax_c14__ax_c16__ax_riotaBAD__df_lsatoms__df_lshyp__df_lcv__df_lfl__df_lkr__df_ldual with wceq clsa (cmpt (λ x0 . cvv) (λ x0 . crn (cmpt (λ x1 . cdif (cfv (cv x0) cbs) (csn (cfv (cv x0) c0g))) (λ x1 . cfv (csn (cv x1)) (cfv (cv x0) clspn))))).

Assume H0: ∀ x0 : ι → ι → ο . ∀ x1 x2 . (∀ x3 . wceq (cv x3) (cv x2)) ⟶ (∀ x3 . x0 x3 x2) ⟶ ∀ x3 . x0 x1 x3.

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

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

Assume H3: ∀ x0 : ι → ο . ∀ x1 x2 . wn (∀ x3 . wceq (cv x3) (cv x1)) ⟶ wceq (cv x2) (cv x1) ⟶ x0 x2 ⟶ ∀ x3 . wceq (cv x3) (cv x1) ⟶ x0 x3.

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

Assume H5: ∀ x0 . wn (∀ x1 . wceq (cv x1) (cv x1)) ⟶ wn (∀ x1 . wceq (cv x1) (cv x1)) ⟶ wceq (cv x0) (cv x0) ⟶ ∀ x1 . wceq (cv x1) (cv x1).

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

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

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

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

...

■

Proofgold Proof