X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Fgrammar%2Flenv_px.ma;h=9de1599e4050336ef539a24b0febad10f7e49d4d;hb=f6464ba2cffc9936b4d8285604786cd91531e0d0;hp=1b0c88e021c03d71a5c83bc0d0b321f44745d3e8;hpb=f79d97a42a84f94d37ad9589fcce46149ee23d12;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_px.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_px.ma
index 1b0c88e02..9de1599e4 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_px.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_px.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/grammar/lenv_length.ma".
+include "basic_2/grammar/lenv_append.ma".
 
 (* POINTWISE EXTENSION OF A CONTEXT-FREE REALTION FOR TERMS *****************)
 
@@ -80,6 +80,10 @@ lemma lpx_refl: ∀R. reflexive ? R → reflexive … (lpx R).
 #R #HR #L elim L -L // /2 width=1/
 qed.
 
+lemma lpx_sym: ∀R. symmetric ? R → symmetric … (lpx R).
+#R #HR #L1 #L2 #H elim H -H // /3 width=1/
+qed.
+
 lemma lpx_trans: ∀R. Transitive ? R → Transitive … (lpx R).
 #R #HR #L1 #L #H elim H -L //
 #I #K1 #K #V1 #V #_ #HV1 #IHK1 #X #H
@@ -129,3 +133,8 @@ lemma lpx_inv_TC: ∀R. reflexive ? R →
                   ∀L1,L2. lpx (TC … R) L1 L2 → TC … (lpx R) L1 L2.
 #R #HR #L1 #L2 #H elim H -L1 -L2 /2 width=1/ /3 width=3/
 qed.
+
+lemma lpx_append: ∀R,K1,K2. lpx R K1 K2 → ∀L1,L2. lpx R L1 L2 →
+                  lpx R (L1 @@ K1) (L2 @@ K2).
+#R #K1 #K2 #H elim H -K1 -K2 // /3 width=1/
+qed.