X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Fgrammar%2Flenv_append.ma;fp=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Fgrammar%2Flenv_append.ma;h=2f693218856771dccd6bd96b156ef5d136b911ae;hb=039f4f6db3a3c128959cd471eb78f575906e07b6;hp=83b65a3353d47ac1f57f3d656cdd0d5338b00f55;hpb=a634c95917dee0fca1d1cf77b6fb7491975128cc;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_append.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_append.ma
index 83b65a335..2f6932188 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_append.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_append.ma
@@ -29,6 +29,10 @@ lemma append_atom_sn: ∀L. ⋆ @@ L = L.
 #L elim L -L normalize //
 qed.
 
+lemma append_assoc: associative … append.
+#L1 #L2 #L3 elim L3 -L3 normalize //
+qed.
+
 lemma append_length: ∀L1,L2. |L1 @@ L2| = |L1| + |L2|.
 #L1 #L2 elim L2 -L2 normalize //
 qed.