| #i #HG #HL #HT #A #HA #b #f #L0 #HL01 #X0 #H0 #L2 #HL20 destruct
elim (aaa_inv_lref_drops … HA) -HA #I #K1 #V1 #HLK1 #HKV1
elim (lifts_inv_lref1 … H0) -H0 #j #Hf #H destruct
| #i #HG #HL #HT #A #HA #b #f #L0 #HL01 #X0 #H0 #L2 #HL20 destruct
elim (aaa_inv_lref_drops … HA) -HA #I #K1 #V1 #HLK1 #HKV1
elim (lifts_inv_lref1 … H0) -H0 #j #Hf #H destruct