apply cons r
α : Type
r : α → α → Prop
inst✝¹ : DecidableRel r
a : α
l : List α
inst✝ : Asymmetric r
a' : α
as : List α
h : Sorted r (a' :: as)
h' : ¬r a a'
⊢ Sorted r (a' :: insert r a as)
case h₁
α : Type
r : α → α → Prop
inst✝¹ : DecidableRel r
a : α
l : List α
inst✝ : Asymmetric r
a' : α
as : List α
h : Sorted r (a' :: as)
h' : ¬r a a'
⊢ Sorted r (insert r a as)

case h₃
α : Type
r : α → α → Prop
inst✝¹ : DecidableRel r
a : α
l : List α
inst✝ : Asymmetric r
a' : α
as : List α
h : Sorted r (a' :: as)
h' : ¬r a a'
⊢ r a' (insert r a as)[0]

case h₂
α : Type
r : α → α → Prop
inst✝¹ : DecidableRel r
a : α
l : List α
inst✝ : Asymmetric r
a' : α
as : List α
h : Sorted r (a' :: as)
h' : ¬r a a'
⊢ List.length (insert r a as) > 0