Apply df_lnop__df_bdop__df_unop__df_hmop__df_nmfn__df_nlfn__df_cnfn__df_lnfn__df_adjh__df_bra__df_kb__df_leop__df_eigvec__df_eigval__df_spec__df_st__df_hst__df_cv with wceq ck (cmpt2 (λ x0 x1 . chil) (λ x0 x1 . chil) (λ x0 x1 . cmpt (λ x2 . chil) (λ x2 . co (co (cv x2) (cv x1) csp) (cv x0) csm))).

Assume H0: wceq clo (crab (λ x0 . wral (λ x1 . wral (λ x2 . wral (λ x3 . wceq (cfv (co (co (cv x1) (cv x2) csm) (cv x3) cva) (cv x0)) (co (co (cv x1) (cfv (cv x2) (cv x0)) csm) (cfv (cv x3) (cv x0)) cva)) (λ x3 . chil)) (λ x2 . chil)) (λ x1 . cc)) (λ x0 . co chil chil cmap)).

Assume H1: wceq cbo (crab (λ x0 . wbr (cfv (cv x0) cnop) cpnf clt) (λ x0 . clo)).

Assume H2: wceq cuo (cab (λ x0 . wa (wfo chil chil (cv x0)) (wral (λ x1 . wral (λ x2 . wceq (co (cfv (cv x1) (cv x0)) (cfv (cv x2) (cv x0)) csp) (co (cv x1) (cv x2) csp)) (λ x2 . chil)) (λ x1 . chil)))).

Assume H3: wceq cho (crab (λ x0 . wral (λ x1 . wral (λ x2 . wceq (co (cv x1) (cfv (cv x2) (cv x0)) csp) (co (cfv (cv x1) (cv x0)) (cv x2) csp)) (λ x2 . chil)) (λ x1 . chil)) (λ x0 . co chil chil cmap)).

Assume H4: wceq cnmf (cmpt (λ x0 . co cc chil cmap) (λ x0 . csup (cab (λ x1 . wrex (λ x2 . wa (wbr (cfv (cv x2) cno) c1 cle) (wceq (cv x1) (cfv (cfv (cv x2) (cv x0)) cabs))) (λ x2 . chil))) cxr clt)).

Assume H5: wceq cnl (cmpt (λ x0 . co cc chil cmap) (λ x0 . cima (ccnv (cv x0)) (csn cc0))).

Assume H6: wceq ccnfn (crab (λ x0 . wral (λ x1 . wral (λ x2 . wrex (λ x3 . wral (λ x4 . wbr (cfv (co (cv x4) (cv x1) cmv) cno) ... ... ⟶ wbr (cfv (co (cfv (cv x4) (cv x0)) (cfv (cv x1) (cv x0)) cmin) cabs) (cv x2) clt) ...) ...) ...) ...) ...).

...

■

Proofgold Proof