induction' l with x xs ih
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a : α
l : List α
ordered : List.Pairwise LE.le l
⊢ List.Pairwise LE.le (insert' a l)
case nil
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a : α
ordered : List.Pairwise LE.le []
⊢ List.Pairwise LE.le (insert' a [])

case cons
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : List.Pairwise LE.le (x :: xs)
⊢ List.Pairwise LE.le (insert' a (x :: xs))