From 05ba7289d4fc9b3b816ecbfabc76656107ee1015 Mon Sep 17 00:00:00 2001
From: bertot
Date: Wed, 19 Aug 2009 09:28:36 +0000
Subject: adds a property on map

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12285 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Lists/List.v | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index dca217d504..9add5f48d4 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -1128,6 +1128,12 @@ Section Map.
 
 End Map. 
 
+Lemma map_id : forall (A :Type) (l : list A),
+  map (fun x => x) l = l.
+Proof.
+  induction l; simpl; auto; rewrite IHl; auto.
+Qed.
+
 Lemma map_map : forall (A B C:Type)(f:A->B)(g:B->C) l, 
   map g (map f l) = map (fun x => g (f x)) l.
 Proof.
-- 
cgit v1.2.3