>(lift_inv_sort1 … H) -H //
| #I #G #L1 #K1 #V1 #B #i #HLK1 #_ #IHB #L2 #d #e #HL21 #T2 #H
elim (lift_inv_lref1 … H) -H * #Hid #H destruct
>(lift_inv_sort1 … H) -H //
| #I #G #L1 #K1 #V1 #B #i #HLK1 #_ #IHB #L2 #d #e #HL21 #T2 #H
elim (lift_inv_lref1 … H) -H * #Hid #H destruct