chore: uncomment cons_injective and cons_inj in Data/List/Basic.lean (#…

…372)

Uncomment two theorems that were added in commented form in #22.

You may compare to the mathlib3 versions here: https://github.com/leanprover-community/mathlib/blob/aaf7dc2c34831dbd92a21b9e37c1f63017d35f45/src/data/list/basic.lean#L50-L54

Mathlib/Data/List/Basic.lean

@@ -50,11 +50,11 @@ theorem tail_eq_of_cons_eq {h₁ h₂ : α} {t₁ t₂ : List α} :
       (h₁::t₁) = (h₂::t₂) → t₁ = t₂ :=
 fun Peq => List.noConfusion Peq (fun _ Pteq => Pteq)
 
--- @[simp] theorem cons_injective {a : α} : injective (cons a) :=
--- assume l₁ l₂, assume Pe, tail_eq_of_cons_eq Pe
+@[simp] theorem cons_injective {a : α} : injective (cons a) :=
+λ _ _ Pe => tail_eq_of_cons_eq Pe
 
--- theorem cons_inj (a : α) {l l' : List α} : a::l = a::l' ↔ l = l' :=
--- cons_injective.eq_iff
+theorem cons_inj (a : α) {l l' : List α} : a::l = a::l' ↔ l = l' :=
+cons_injective.eq_iff
 
 theorem exists_cons_of_ne_nil {l : List α} (h : l ≠ nil) : ∃ b L, l = b :: L := by
   cases l with