+lemma lexs_inv_tl: ∀RN,RP,f,I,L1,L2,V1,V2. L1 ⦻*[RN, RP, ⫱f] L2 →
+ RN L1 V1 V2 → RP L1 V1 V2 →
+ L1.ⓑ{I}V1 ⦻*[RN, RP, f] L2.ⓑ{I}V2.
+#RN #RP #f #I #L2 #L2 #V1 #V2 elim (pn_split f) *
+/2 width=1 by lexs_next, lexs_push/
+qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma lexs_fwd_pair: ∀RN,RP,f,I1,I2,L1,L2,V1,V2.
+ L1.ⓑ{I1}V1 ⦻*[RN, RP, f] L2.ⓑ{I2}V2 →
+ L1 ⦻*[RN, RP, ⫱f] L2 ∧ I1 = I2.
+#RN #RP #f #I1 #I2 #L2 #L2 #V1 #V2 #Hf
+elim (pn_split f) * #g #H destruct
+[ elim (lexs_inv_push … Hf) | elim (lexs_inv_next … Hf) ] -Hf
+/2 width=1 by conj/
+qed-.
+