+(* Basic forward lemmas *****************************************************)
+
+lemma lexs_fwd_pair: ∀RN,RP,I1,I2,L1,L2,V1,V2,f.
+ L1.ⓑ{I1}V1 ⦻*[RN, RP, f] L2.ⓑ{I2}V2 →
+ L1 ⦻*[RN, RP, ⫱f] L2 ∧ I1 = I2.
+#RN #RP #I1 #I2 #L2 #L2 #V1 #V2 #f #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-.
+