X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fbasics%2Flists%2Flist.ma;h=edc049738b5c5a5f01b98698dc6ac1fadec15d87;hb=43f6de7986407cb15b5b39b18eb59d19d0abfd20;hp=c59f828261270988169b151f6f2c914e8262a54e;hpb=7d58d5dc7f897622f2010326023b17c6592d5f03;p=helm.git

diff --git a/matita/matita/lib/basics/lists/list.ma b/matita/matita/lib/basics/lists/list.ma
index c59f82826..edc049738 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.
 
@@ -225,7 +225,7 @@ qed.
 lemma split_len: ∀A,n,l. n ≤ |l| →
   |\fst (split A l n)| = n.
 #A #n #l #Hlen normalize >(eq_pair_fst_snd ?? (split_rev …))
-normalize >lenght_reverse  >(split_rev_len … [ ] Hlen) normalize //
+normalize >length_reverse  >(split_rev_len … [ ] Hlen) normalize //
 qed.
   
 lemma split_rev_eq: ∀A,n,l,acc. n ≤ |l| →