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

more typos
---

diff --git a/matita/matita/lib/basics/lists/list.ma b/matita/matita/lib/basics/lists/list.ma
index 8c508108d..edc049738 100644
--- a/matita/matita/lib/basics/lists/list.ma
+++ b/matita/matita/lib/basics/lists/list.ma
@@ -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| →