simp [h']
case pos
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
h : ¬tail = []
h' : head ≤ smallest tail h
⊢ (∀ (h : ¬tail = []), head ≤ smallest tail h) ∨ min head (smallest tail h) ∈ tail
no goals