Apply df_odz__df_phi__df_pc__df_gz__df_vdwap__df_vdwmc__df_vdwpc__df_ram__df_prmo__df_struct__df_ndx__df_slot__df_base__df_sets__df_ress__df_plusg__df_mulr__df_starv with
wceq cvdwa (cmpt (λ x0 . cn0) (λ x0 . cmpt2 (λ x1 x2 . cn) (λ x1 x2 . cn) (λ x1 x2 . crn (cmpt (λ x3 . co cc0 (co (cv x0) c1 cmin) cfz) (λ x3 . co (cv x1) (co (cv x3) (cv x2) cmul) caddc))))).