the partial commit continues ...

[helm.git] / matita / matita / contribs / lambda_delta / basic_2 / grammar / lenv_append.ma

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 83b65a3353d47ac1f57f3d656cdd0d5338b00f55..2f693218856771dccd6bd96b156ef5d136b911ae 100644 (file)
--- 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.