@or_intror @(cpxs_trans … HU) -U /3 width=1/ (**) (* explicit constructor *)
| #b #V1 #V2 #V0 #T1 #_ #_ #HT1 #_
elim (cpxs_inv_abst1 … HT1) -HT1 #W2 #T2 #_ #_ #H destruct
@or_intror @(cpxs_trans … HU) -U /3 width=1/ (**) (* explicit constructor *)
| #b #V1 #V2 #V0 #T1 #_ #_ #HT1 #_
elim (cpxs_inv_abst1 … HT1) -HT1 #W2 #T2 #_ #_ #H destruct