Apply df_bj_rrvec__df_tau__df_finxp__ax_luk1__ax_luk2__ax_luk3__ax_wl_13v__ax_wl_11v__ax_wl_8cl__df_wl_clelv2__df_totbnd__df_bnd__df_ismty__df_rrn__df_ass__df_exid__df_mgmOLD__df_sgrOLD with ∀ x0 x1 : ο . x0 ⟶ wn x0 ⟶ x1.

Assume H0: wceq crrvec (crab (λ x0 . wceq (cfv (cv x0) csca) crefld) (λ x0 . clvec)).

Assume H1: wceq ctau (cinf (cin crp (cima (ccnv ccos) (csn c1))) cr clt).

Assume H2: ∀ x0 x1 : ι → ο . wceq (cfinxp x0 x1) (cab (λ x2 . wa (wcel x1 com) (wceq c0 (cfv x1 (crdg (cmpt2 (λ x3 x4 . com) (λ x3 x4 . cvv) (λ x3 x4 . cif (wa (wceq (cv x3) c1o) (wcel (cv x4) x0)) c0 (cif (wcel (cv x4) (cxp cvv x0)) (cop (cuni (cv x3)) (cfv (cv x4) c1st)) (cop (cv x3) (cv x4))))) (cop x1 (cv x2))))))).

Assume H3: ∀ x0 x1 x2 : ο . (x0 ⟶ x1) ⟶ (x1 ⟶ x2) ⟶ x0 ⟶ x2.

Assume H4: ∀ x0 : ο . (wn x0 ⟶ x0) ⟶ x0.

Assume H5: ∀ x0 x1 : ο . x0 ⟶ wn x0 ⟶ x1.

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

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

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

Assume H9: ∀ x0 : ι → ι → ο . ∀ x1 . wb (wcel2_wl (λ x2 . x0 x2)) (∀ x2 . wceq (cv x2) (cv x1) ⟶ wcel_wl (λ x3 . x0 x1)).

Assume H10: wceq ctotbnd (cmpt (λ x0 . cvv) (λ x0 . crab (λ x1 . wral (λ x2 . wrex (λ x3 . wa (wceq (cuni (cv x3)) (cv x0)) (wral (λ x4 . wrex (λ x5 . wceq (cv x4) (co (cv x5) (cv x2) (cfv (cv x1) cbl))) (λ x5 . cv x0)) (λ x4 . cv x3))) (λ x3 . cfn)) (λ x2 . crp)) (λ x1 . cfv (cv x0) cme))).

Assume H11: wceq cbnd (cmpt (λ x0 . cvv) (λ x0 . crab (λ x1 . wral (λ x2 . wrex (λ x3 . wceq (cv x0) (co (cv x2) (cv x3) (cfv (cv x1) cbl))) (λ x3 . crp)) (λ x2 . cv x0)) (λ x1 . cfv (cv x0) cme))).

...

■

Proofgold Proof