>(lift_inv_sort1 … H) -X -K -l -m //
| #I #G #K #K0 #V #i #HK0 #_ #IHV #L #s #l #m #HLK #X #H
elim (lift_inv_lref1 … H) * #Hil #H destruct
>(lift_inv_sort1 … H) -X -K -l -m //
| #I #G #K #K0 #V #i #HK0 #_ #IHV #L #s #l #m #HLK #X #H
elim (lift_inv_lref1 … H) * #Hil #H destruct