induction' l with y ys ih
case mpr
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a : α
l : List α
hor : x = a ∨ x ∈ l
⊢ x ∈ insert' a l
case mpr.nil
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a : α
hor : x = a ∨ x ∈ []
⊢ x ∈ insert' a []

case mpr.cons
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
hor : x = a ∨ x ∈ y :: ys
⊢ x ∈ insert' a (y :: ys)