have c'' : tail ≠ [] := by
  intro contra
  rw [contra] at hyp'
  contradiction
case right
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
a : ℕ
hyp' : a ∈ tail
⊢ (if c : tail = [] then head else Nat.min head (smallest tail c)) ≤ a
case right
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
a : ℕ
hyp' : a ∈ tail
c'' : tail ≠ []
⊢ (if c : tail = [] then head else Nat.min head (smallest tail c)) ≤ a