apply insert_sorted_of_sorted f <| sorted_of_insertSort as
α : Type
f : α → α → Bool
r : α → α → Prop
l : List α
inst✝ : Asymmetric f
a : α
as : List α
⊢ Sorted f (insert f a (insertSort f as))
no goals