Apply df_ch__df_oc__df_ch0__df_shs__df_span__df_chj__df_chsup__df_pjh__df_cm__df_hosum__df_homul__df_hodif__df_hfsum__df_hfmul__df_h0op__df_iop__df_nmop__df_cnop with wceq chsup (cmpt (λ x0 . cpw (cpw chil)) (λ x0 . cfv (cfv (cuni (cv x0)) cort) cort)).

Assume H0: wceq cch (crab (λ x0 . wss (cima chli (co (cv x0) cn cmap)) (cv x0)) (λ x0 . csh)).

Assume H1: wceq cort (cmpt (λ x0 . cpw chil) (λ x0 . crab (λ x1 . wral (λ x2 . wceq (co (cv x1) (cv x2) csp) cc0) (λ x2 . cv x0)) (λ x1 . chil))).

Assume H2: wceq c0h (csn c0v).

Assume H3: wceq cph (cmpt2 (λ x0 x1 . csh) (λ x0 x1 . csh) (λ x0 x1 . cima cva (cxp (cv x0) (cv x1)))).

Assume H4: wceq cspn (cmpt (λ x0 . cpw chil) (λ x0 . cint (crab (λ x1 . wss (cv x0) (cv x1)) (λ x1 . csh)))).

Assume H5: wceq chj (cmpt2 (λ x0 x1 . cpw chil) (λ x0 x1 . cpw chil) (λ x0 x1 . cfv (cfv (cun (cv x0) (cv x1)) cort) cort)).

Assume H6: wceq chsup (cmpt (λ x0 . cpw (cpw chil)) (λ x0 . cfv (cfv (cuni (cv x0)) cort) cort)).

Assume H7: wceq cpjh (cmpt (λ x0 . cch) (λ x0 . cmpt (λ x1 . chil) (λ x1 . crio (λ x2 . wrex (λ x3 . wceq (cv x1) (co (cv x2) (cv x3) cva)) (λ x3 . cfv (cv x0) cort)) (λ x2 . cv x0)))).

Assume H8: wceq ccm (copab (λ x0 x1 . wa (wa (wcel (cv x0) cch) (wcel (cv x1) cch)) (wceq (cv x0) (co (cin (cv x0) (cv x1)) (cin (cv x0) (cfv (cv x1) cort)) chj)))).

Assume H9: wceq chos (cmpt2 (λ x0 x1 . co chil chil cmap) (λ x0 x1 . co chil chil cmap) (λ x0 x1 . cmpt (λ x2 . chil) (λ x2 . co (cfv (cv x2) (cv x0)) (cfv (cv x2) (cv x1)) cva))).

Assume H10: wceq chot (cmpt2 (λ x0 x1 . cc) (λ x0 x1 . co chil chil cmap) (λ x0 x1 . cmpt (λ x2 . chil) (λ x2 . co (cv x0) (cfv (cv x2) (cv x1)) csm))).

Assume H11: wceq chod (cmpt2 ... ... ...).

...

■

Proofgold Proof