Apply df_pj__df_hil__df_obs__df_dsmm__df_frlm__df_uvc__df_lindf__df_linds__df_mamu__df_mat__df_dmat__df_scmat__df_mvmul__df_marrep__df_marepv__df_subma__df_mdet__df_madu with wceq cmatrepV (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . cmpt2 (λ x2 x3 . cfv (co (cv x0) (cv x1) cmat) cbs) (λ x2 x3 . co (cfv (cv x1) cbs) (cv x0) cmap) (λ x2 x3 . cmpt (λ x4 . cv x0) (λ x4 . cmpt2 (λ x5 x6 . cv x0) (λ x5 x6 . cv x0) (λ x5 x6 . cif (wceq (cv x6) (cv x4)) (cfv (cv x5) (cv x3)) (co (cv x5) (cv x6) (cv x2))))))).

Assume H0: wceq cpj (cmpt (λ x0 . cvv) (λ x0 . cin (cmpt (λ x1 . cfv (cv x0) clss) (λ x1 . co (cv x1) (cfv (cv x1) (cfv (cv x0) cocv)) (cfv (cv x0) cpj1))) (cxp cvv (co (cfv (cv x0) cbs) (cfv (cv x0) cbs) cmap)))).

Assume H1: wceq chs (crab (λ x0 . wceq (cdm (cfv (cv x0) cpj)) (cfv (cv x0) ccss)) (λ x0 . cphl)).

Assume H2: wceq cobs (cmpt (λ x0 . cphl) (λ x0 . crab (λ x1 . wa (wral (λ x2 . wral (λ x3 . wceq (co (cv x2) (cv x3) (cfv (cv x0) cip)) (cif (wceq (cv x2) (cv x3)) (cfv (cfv (cv x0) csca) cur) (cfv (cfv (cv x0) csca) c0g))) (λ x3 . cv x1)) (λ x2 . cv x1)) (wceq (cfv (cv x1) (cfv (cv x0) cocv)) (csn (cfv (cv x0) c0g)))) (λ x1 . cpw (cfv (cv x0) cbs)))).

Assume H3: wceq cdsmm (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . co (co (cv x0) (cv x1) cprds) (crab (λ x2 . wcel (crab (λ x3 . wne (cfv (cv x3) (cv x2)) (cfv (cfv (cv x3) (cv x1)) c0g)) (λ x3 . cdm (cv x1))) cfn) (λ x2 . cixp (λ x3 . cdm (cv x1)) (λ x3 . cfv (cfv (cv x3) (cv x1)) cbs))) cress)).

Assume H4: wceq cfrlm (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . co (cv x0) (cxp (cv x1) ...) ...)).

...

■

Proofgold Proof