cases heq
case cons.refine_1
α : Type u
β : Type v
a : α
l : List α
IH : (∀ (i j : Nat) (x : i < length l) (x_1 : j < length l), l[i] = l[j] → i = j) → Nodup l
h : ∀ (i j : Nat) (x : i < length (a :: l)) (x_1 : j < length (a :: l)), (a :: l)[i] = (a :: l)[j] → i = j
a'✝ : α
hmem : a'✝ ∈ l
heq : a = a'✝
⊢ False
case cons.refine_1.refl
α : Type u
β : Type v
a : α
l : List α
IH : (∀ (i j : Nat) (x : i < length l) (x_1 : j < length l), l[i] = l[j] → i = j) → Nodup l
h : ∀ (i j : Nat) (x : i < length (a :: l)) (x_1 : j < length (a :: l)), (a :: l)[i] = (a :: l)[j] → i = j
hmem : a ∈ l
⊢ False