-lemma lfsx_lref_pair: ∀h,o,G,K,V. ⦃G, K⦄ ⊢ ⬈*[h, o] 𝐒⦃V⦄ → G ⊢ ⬈*[h, o, V] 𝐒⦃K⦄ →
- ∀I,L,i. ⬇*[i] L ≡ K.ⓑ{I}V → G ⊢ ⬈*[h, o, #i] 𝐒⦃L⦄.
-#h #o #G #K #V #HV #HK #I #L #i #HLK
-@(lfsx_lifts … (#0) … HLK) -L /2 width=3 by lfsx_pair_lpxs/
+lemma lfsx_lref_pair_drops: ∀h,o,G,K,V. ⦃G, K⦄ ⊢ ⬈*[h, o] 𝐒⦃V⦄ → G ⊢ ⬈*[h, o, V] 𝐒⦃K⦄ →
+ ∀I,i,L. ⬇*[i] L ≡ K.ⓑ{I}V → G ⊢ ⬈*[h, o, #i] 𝐒⦃L⦄.
+#h #o #G #K #V #HV #HK #I #i elim i -i
+[ #L #H >(drops_fwd_isid … H) -H /2 width=3 by lfsx_pair_lpxs/
+| #i #IH #L #H
+ elim (drops_inv_bind2_isuni_next … H) -H // #J #Y #HY #H destruct
+ @(lfsx_lifts … (𝐔❴1❵)) /3 width=6 by drops_refl, drops_drop/ (**) (* full auto fails *)
+]