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 cdmat (cmpt2 (λ x0 x1 . cfn) (λ x0 x1 . cvv) (λ x0 x1 . crab (λ x2 . wral (λ x3 . wral (λ x4 . wne (cv x3) (cv x4) ⟶ wceq (co (cv x3) (cv x4) (cv x2)) (cfv (cv x1) c0g)) (λ x4 . cv x0)) (λ x3 . cv x0)) (λ x2 . cfv (co (cv x0) (cv x1) cmat) cbs))).

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) (csn (cfv (cv x0) crglmod))) cdsmm)).

Assume H5: wceq cuvc (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) ...).

...

■

Proofgold Proof