Add map_cons from Coq 8.6

1 files changed, 11 insertions, 0 deletions

diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v
index 06e7206cd..9c263eed9 100644
--- a/src/Util/ListUtil.v
+++ b/src/Util/ListUtil.v
@@ -49,6 +49,17 @@ Module Export List.
   Local Set Implicit Arguments.
   Import ListNotations.
   (** From the 8.6 Standard Library *)
+
+  Section Map.
+    Variables (A : Type) (B : Type).
+    Variable f : A -> B.
+
+    Lemma map_cons (x:A)(l:list A) : map f (x::l) = (f x) :: (map l).
+    Proof.
+      reflexivity.
+    Qed.
+  End Map.
+
   Lemma in_seq len start n :
     In n (seq start len) <-> start <= n < start+len.
   Proof.