Apply df_msub__df_mvh__df_mpst__df_msr__df_msta__df_mfs__df_mcls__df_mpps__df_mthm__df_m0s__df_msa__df_mwgfs__df_msyn__df_mtree__df_mst__df_msax__df_mufs__df_muv with
wceq cmthm (cmpt (λ x0 . cvv) (λ x0 . cima (ccnv (cfv (cv x0) cmsr)) (cima (cfv (cv x0) cmsr) (cfv (cv x0) cmpps)))).