+(* Basic_2A1: was: lsx_lpx_trans *)
+lemma lfsx_lfpx_trans: āh,o,G,L1,T. G ā¢ ā¬*[h, o, T] šā¦L1ā¦ ā
+ āL2. ā¦G, L1ā¦ ā¢ ā¬[h, T] L2 ā G ā¢ ā¬*[h, o, T] šā¦L2ā¦.
+#h #o #G #L1 #T #H @(lfsx_ind ā¦ H) -L1 #L1 #HL1 #IHL1 #L2 #HL12
+elim (lfdeq_dec h o L1 L2 T) /3 width=4 by lfsx_lfdeq_trans, lfxs_refl/
+qed-.
+