apply cons f
α : Type
f : α → α → Bool
r : α → α → Prop
a : α
l : List α
inst✝ : Asymmetric f
a' : α
as : List α
h : Sorted f (a' :: as)
h' : f a a' = false
⊢ Sorted f (a' :: insert f a as)
case h₁
α : Type
f : α → α → Bool
r : α → α → Prop
a : α
l : List α
inst✝ : Asymmetric f
a' : α
as : List α
h : Sorted f (a' :: as)
h' : f a a' = false
⊢ Sorted f (insert f a as)

case h₃
α : Type
f : α → α → Bool
r : α → α → Prop
a : α
l : List α
inst✝ : Asymmetric f
a' : α
as : List α
h : Sorted f (a' :: as)
h' : f a a' = false
⊢ f a' (insert f a as)[0] = true

case h₂
α : Type
f : α → α → Bool
r : α → α → Prop
a : α
l : List α
inst✝ : Asymmetric f
a' : α
as : List α
h : Sorted f (a' :: as)
h' : f a a' = false
⊢ List.length (insert f a as) > 0