X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frestricted%2Flpqs.ma;h=686ea1d69132c45b6aaf2a296ca45d192f7ab582;hb=713673ecf863cb6187291f016ed4490b12a03ac0;hp=8a6f8e8c427d080c471aaadaff88bf4c7365b0e7;hpb=520d4370a540a98f5e5e1d85acfef0c982cc1e04;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/restricted/lpqs.ma b/matita/matita/contribs/lambdadelta/basic_2/restricted/lpqs.ma
index 8a6f8e8c4..686ea1d69 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/restricted/lpqs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/restricted/lpqs.ma
@@ -40,7 +40,6 @@ lemma lpqs_inv_pair2: ∀I,L1,K2,V2. L1 ⊢ ➤* K2. ⓑ{I} V2 →
 
 (* Basic properties *********************************************************)
 
-(* Basic_1: was by definition: csubst1_refl *)
 lemma lpqs_refl: ∀L. L ⊢ ➤* L.
 /2 width=1 by lpx_sn_refl/ qed.
 
@@ -56,3 +55,13 @@ qed.
 
 lemma lpqs_fwd_length: ∀L1,L2. L1 ⊢ ➤* L2 → |L1| = |L2|.
 /2 width=2 by lpx_sn_fwd_length/ qed-.
+
+(* 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-.