simp [insert]
α : Type
r : α → α → Prop
inst✝ : DecidableRel r
a a' : α
as : List α
h' : r a' a
h : Sorted r [a']
⊢ r a' (insert r a [])[0]
α : Type
r : α → α → Prop
inst✝ : DecidableRel r
a a' : α
as : List α
h' : r a' a
h : Sorted r [a']
⊢ r a' a