-[ #k #d #e #U1 #HU1 #U2 #HU2
- lapply (lift_mono … HU1 … HU2) -HU1 #H destruct -U1;
- lapply (lift_inv_sort1 … HU2) -HU2 #H destruct -U2 //
-| #i #d #e #U1 #HU1 #U2 #HU2
- lapply (lift_mono … HU1 … HU2) -HU1 #H destruct -U1;
- lapply (lift_inv_lref1 … HU2) * * #Hid #H destruct -U2 //
+[ * #i #d #e #U1 #HU1 #U2 #HU2
+ 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 //
+ ]