split
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
⊢ (∀ (h : ¬tail = []), head ≤ smallest tail h) ∨ (if c : tail = [] then head else min head (smallest tail c)) ∈ tail
case inl
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
h✝ : tail = []
⊢ (∀ (h : ¬tail = []), head ≤ smallest tail h) ∨ head ∈ tail

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