]> matita.cs.unibo.it Git - helm.git/commitdiff
more typos
authorAndrea Asperti <andrea.asperti@unibo.it>
Mon, 28 May 2012 12:13:49 +0000 (12:13 +0000)
committerAndrea Asperti <andrea.asperti@unibo.it>
Mon, 28 May 2012 12:13:49 +0000 (12:13 +0000)
matita/matita/lib/basics/lists/list.ma

index 8c508108d8faa4c78ddce9cf9d15f5a9943bd211..edc049738b5c5a5f01b98698dc6ac1fadec15d87 100644 (file)
@@ -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| →