From dc7d29345821b84070bc5d235772c598c10d07c3 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 28 May 2012 12:11:59 +0000 Subject: [PATCH] typos --- matita/matita/lib/basics/lists/list.ma | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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. -- 2.39.2