+(* Advanced forward lemmas **************************************************)
+
+lemma lsx_fwd_lref_be: ∀h,g,I,G,L,d,i. d ≤ yinj i → G ⊢ ⬊*[h, g, #i, d] L →
+ ∀K,V. ⇩[i] L ≡ K.ⓑ{I}V → G ⊢ ⬊*[h, g, V, 0] K.
+#h #g #I #G #L #d #i #Hdi #H @(lsx_ind … H) -L
+#L1 #_ #IHL1 #K1 #V #HLK1 @lsx_intro
+#K2 #HK12 #HnK12 lapply (ldrop_fwd_drop2 … HLK1)
+#H2LK1 elim (ldrop_lpx_trans … H2LK1 … HK12) -H2LK1 -HK12
+#L2 #HL12 #H2LK2 #H elim (leq_ldrop_conf_be … H … HLK1) -H /2 width=1 by ylt_inj/
+#Y #_ #HLK2 lapply (ldrop_fwd_drop2 … HLK2)
+#HY lapply (ldrop_mono … HY … H2LK2) -HY -H2LK2 #H destruct
+/4 width=10 by lleq_inv_lref_ge/
+qed-.
+