[ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=3/
| elim (lift_inv_lref2 … H) -H * #Hid #H destruct /3 width=3/
| lapply (lift_inv_gref2 … H) -H #H destruct /2 width=3/
]
| #L #LV #V #V2 #W2 #i #HLV #HV2 #HVW2 #IHV2 #K #d #e #HLK #T1 #H
elim (lift_inv_lref2 … H) -H * #Hid #H destruct
[ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=3/
| elim (lift_inv_lref2 … H) -H * #Hid #H destruct /3 width=3/
| lapply (lift_inv_gref2 … H) -H #H destruct /2 width=3/
]
| #L #LV #V #V2 #W2 #i #HLV #HV2 #HVW2 #IHV2 #K #d #e #HLK #T1 #H
elim (lift_inv_lref2 … H) -H * #Hid #H destruct