elim (cnv_inv_bind … HWU) -HWU #HW #HU
elim (cnv_inv_bind … HWT) -HWT #_ #HT
elim (cpms_inv_abst_sn … HUX) -HUX #W0 #X0 #_ #HUX0 #H destruct
elim (cnv_inv_bind … HWU) -HWU #HW #HU
elim (cnv_inv_bind … HWT) -HWT #_ #HT
elim (cpms_inv_abst_sn … HUX) -HUX #W0 #X0 #_ #HUX0 #H destruct