(* Advanced properties ******************************************************)
(* Basic_2A1: uses: lsx_lleq_trans *)
lemma lfsx_lfdeq_trans: ∀h,o,G,L1,T. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄ →
(* Advanced properties ******************************************************)
(* Basic_2A1: uses: lsx_lleq_trans *)
lemma lfsx_lfdeq_trans: ∀h,o,G,L1,T. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄ →