intro contra
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
a : ℕ
hyp' : a ∈ tail
⊢ tail ≠ []
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
a : ℕ
hyp' : a ∈ tail
contra : tail = []
⊢ False