+
+(* Advanced forward lemmas **************************************************)
+
+lemma lpqs_fwd_append1: ∀K1,L1,L. K1 @@ L1 ⊢ ➤* L →
+ ∃∃K2,L2. K1 ⊢ ➤* K2 & L = K2 @@ L2.
+/2 width=2 by lpx_sn_fwd_append1/ qed-.
+
+lemma lpqs_fwd_append2: ∀L,K2,L2. L ⊢ ➤* K2 @@ L2 →
+ ∃∃K1,L1. K1 ⊢ ➤* K2 & L = K1 @@ L1.
+/2 width=2 by lpx_sn_fwd_append2/ qed-.