elim (lift_inv_lref1 … HX) -HX * #Hid2 #HX destruct /3 width=3/ /4 width=3/
| #i #d1 #e1 #Hid1 #d2 #e2 #X #HX #Hd21
lapply (transitive_le … Hd21 Hid1) -Hd21 #Hid2
elim (lift_inv_lref1 … HX) -HX * #Hid2 #HX destruct /3 width=3/ /4 width=3/
| #i #d1 #e1 #Hid1 #d2 #e2 #X #HX #Hd21
lapply (transitive_le … Hd21 Hid1) -Hd21 #Hid2