- lapply (cpmhe_abst … HWU0) -HWU0 #HWU0
- elim (cnv_cpmhe_mono … H2W … HWU0 … HWX) #_ #H -a -n -n0 -W
- elim (theq_inv_pair1 … H) -V0 -U0 #V0 #U0 #H destruct
+ lapply (cpmuwe_abst … HWU0) -HWU0 #HWU0
+ elim (cnv_cpmuwe_mono … H2W … HWU0 … HWX) #_ #H -a -n -n0 -W
+ elim (tweq_inv_abst_sn … H) -V0 -U0 #V0 #U0 #H destruct