From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Mon, 28 May 2012 12:11:59 +0000 (+0000)
Subject: typos
X-Git-Tag: make_still_working~1685
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=dc7d29345821b84070bc5d235772c598c10d07c3;p=helm.git

typos
---

diff --git a/matita/matita/lib/basics/lists/list.ma b/matita/matita/lib/basics/lists/list.ma
index c59f82826..8c508108d 100644
--- a/matita/matita/lib/basics/lists/list.ma
+++ b/matita/matita/lib/basics/lists/list.ma
@@ -183,13 +183,13 @@ lemma length_map: ∀A,B,l.∀f:A→B. length ? (map ?? f l) = length ? l.
 #A #B #l #f elim l // #a #tl #Hind normalize //
 qed.
 
-lemma lenght_rev_append: ∀A.∀l,acc:list A. 
+lemma length_rev_append: ∀A.∀l,acc:list A. 
   |rev_append ? l acc| = |l|+|acc|.
 #A #l elim l // #a #tl #Hind normalize 
 #acc >Hind normalize // 
 qed.
 
-lemma lenght_reverse: ∀A.∀l:list A. 
+lemma length_reverse: ∀A.∀l:list A. 
   |reverse A l| = |l|.
 // qed.