exact smallest_le tail c'' a hyp'
case right.h
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
a : α
hyp' : a ∈ tail
c'' : tail ≠ []
⊢ smallest tail (_ : ¬tail = []) ≤ a
no goals