feat(library/data/list/basic): add cons related equalities

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.
 -/

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