(* Advanced properties ******************************************************)
+(* Basic_2A1: was just: lsx_lleq_trans *)
lemma lfsx_lfdeq_trans: āh,o,G,L1,T. G ā¢ ā¬*[h, o, T] šā¦L1ā¦ ā
āL2. L1 ā”[h, o, T] L2 ā G ā¢ ā¬*[h, o, T] šā¦L2ā¦.
#h #o #G #L1 #T #H @(lfsx_ind ā¦ H) -L1
/4 width=5 by lfdeq_repl/
qed-.
+(* 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-.
+
(* Advanced forward lemmas **************************************************)
(* Basic_2A1: includes: lsx_fwd_bind_sn lsx_fwd_flat_sn *)
/6 width=4 by lfsx_lfdeq_trans, lfdeq_trans, lfdeq_fwd_pair_sn/
qed-.
-
(* Basic_2A1: was: lsx_fwd_flat_dx *)
lemma lfsx_fwd_flat_dx: āh,o,I,G,L,V,T. G ā¢ ā¬*[h, o, ā{I}V.T] šā¦Lā¦ ā
G ā¢ ā¬*[h, o, T] šā¦Lā¦.