simpa [insert, h'']
α : Type
f : α → α → Bool
r : α → α → Prop
a a' : α
as : List α
h' : f a' a = true
a'' : α
as' : List α
h : Sorted f (a' :: a'' :: as')
h'' : f a a'' = true
⊢ f a' (insert f a (a'' :: as'))[0] = true
no goals