-(* Advanced forward lemmas **************************************************)
-
-lemma lpr_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 lpr_fwd_append2: ∀L,K2,L2. L ⊢ ➡ K2 @@ L2 →
- ∃∃K1,L1. K1 ⊢ ➡ K2 & L = K1 @@ L1.
-/2 width=2 by lpx_sn_fwd_append2/ qed-.
-