From ef4b4d19cef62c8853ffb6f7add1d1f1aa7b180f Mon Sep 17 00:00:00 2001
From: Haitao Zhang <zhtprog@gmail.com>
Date: Sun, 14 Jun 2015 16:45:01 -0700
Subject: [PATCH] feat(library/data/list/basic): add cons related equalities

---
 library/data/fin.lean        |  2 +-
 library/data/list/basic.lean | 11 +++++++++++
 2 files changed, 12 insertions(+), 1 deletion(-)

diff --git a/library/data/fin.lean b/library/data/fin.lean
index 23a671afa..44ed032ed 100644
--- a/library/data/fin.lean
+++ b/library/data/fin.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2015 Haitao Zhang. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Author: Haitao Zhang
+Authors: Haitao Zhang, Leonardo de Moura
 
 Finite ordinal types.
 -/
diff --git a/library/data/list/basic.lean b/library/data/list/basic.lean
index 2ae6527e2..14032bfae 100644
--- a/library/data/list/basic.lean
+++ b/library/data/list/basic.lean
@@ -21,6 +21,17 @@ variable {T : Type}
 lemma cons_ne_nil (a : T) (l : list T) : a::l ≠ [] :=
 by contradiction
 
+lemma head_eq_of_cons_eq {A : Type} {h₁ h₂ : A} {t₁ t₂ : list A} :
+      (h₁::t₁) = (h₂::t₂) → h₁ = h₂ :=
+assume Peq, list.no_confusion Peq (assume Pheq Pteq, Pheq)
+
+lemma tail_eq_of_cons_eq {A : Type} {h₁ h₂ : A} {t₁ t₂ : list A} :
+      (h₁::t₁) = (h₂::t₂) → t₁ = t₂ :=
+assume Peq, list.no_confusion Peq (assume Pheq Pteq, Pteq)
+
+lemma cons_inj {A : Type} {a : A} : injective (cons a) :=
+take l₁ l₂, assume Pe, tail_eq_of_cons_eq Pe
+
 /- append -/
 
 definition append : list T → list T → list T