lapply (lift_mono … HU1 … HU2) -HU1 #H destruct -U1
[ lapply (lift_inv_sort1 … HU2) -HU2 #H destruct -U2 //
| lapply (lift_inv_lref1 … HU2) * * #Hid #H destruct -U2 //
lapply (lift_mono … HU1 … HU2) -HU1 #H destruct -U1
[ lapply (lift_inv_sort1 … HU2) -HU2 #H destruct -U2 //
| lapply (lift_inv_lref1 … HU2) * * #Hid #H destruct -U2 //