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 cph (cmpt2 (λ x0 x1 . csh) (λ x0 x1 . csh) (λ x0 x1 . cima cva (cxp (cv x0) (cv x1)))).