>(lift_inv_sort2 … H) -X /2 width=1 by da_sort/
| #G #L2 #K2 #V2 #i #l #HLK2 #HV2 #IHV2 #L1 #s #d #e #HL21 #X #H
elim (lift_inv_lref2 … H) * #Hid #H destruct [ -HV2 | -IHV2 ]
>(lift_inv_sort2 … H) -X /2 width=1 by da_sort/
| #G #L2 #K2 #V2 #i #l #HLK2 #HV2 #IHV2 #L1 #s #d #e #HL21 #X #H
elim (lift_inv_lref2 … H) * #Hid #H destruct [ -HV2 | -IHV2 ]