X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Flist%2Flist.ma;h=077e1af6c443682939461692d20bdfc20f60be22;hb=7c4bb1d1baed259e4301d4cf0ecca7a0e3885d92;hp=19866cc2992499df10a53a9c0fba8766458c601f;hpb=82baf094141d9ef518d681b8cebcc180bca14d2c;p=helm.git

diff --git a/helm/software/matita/library/list/list.ma b/helm/software/matita/library/list/list.ma
index 19866cc29..077e1af6c 100644
--- a/helm/software/matita/library/list/list.ma
+++ b/helm/software/matita/library/list/list.ma
@@ -195,3 +195,9 @@ intros;elim l
      [simplify;apply le_S_S;assumption
      |simplify;apply le_S;assumption]]
 qed.
+
+lemma length_append : ∀A,l,m.length A (l@m) = length A l + length A m.
+intros;elim l
+[reflexivity
+|simplify;rewrite < H;reflexivity]
+qed.