by_cases c:tail = []
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
⊢ smallest (head :: tail) hyp ∈ head :: tail
case pos
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
c : tail = []
⊢ smallest (head :: tail) hyp ∈ head :: tail

case neg
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
c : ¬tail = []
⊢ smallest (head :: tail) hyp ∈ head :: tail