-[ #L #k #dt #et #K #d #e #_ #T1 #H #_
- lapply (lift_inv_sort2 … H) -H #H destruct -T1 /2/
-| #L #i #dt #et #K #d #e #_ #T1 #H #_
- elim (lift_inv_lref2 … H) -H * #Hid #H destruct -T1 /3/
+[ #L * #i #dt #et #K #d #e #_ #T1 #H #_
+ [ lapply (lift_inv_sort2 … H) -H #H destruct -T1 /2/
+ | elim (lift_inv_lref2 … H) -H * #Hid #H destruct -T1 /3/
+ ]