From ae14e3f084ff70d37842603fa41800641e08b51a Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 28 May 2012 12:13:49 +0000 Subject: [PATCH] more typos --- matita/matita/lib/basics/lists/list.ma | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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| → -- 2.39.2