| #j #f #X1 #H1 #X2 #H2
elim (lifts_inv_lref2 … H1) -H1 #i1 #Hj1 #H destruct
elim (lifts_inv_lref2 … H2) -H2 #i2 #Hj2 #H destruct
| #j #f #X1 #H1 #X2 #H2
elim (lifts_inv_lref2 … H1) -H1 #i1 #Hj1 #H destruct
elim (lifts_inv_lref2 … H2) -H2 #i2 #Hj2 #H destruct