intro hel
case mp
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a : α
l : List α
⊢ x ∈ insert' a l → x = a ∨ x ∈ l
case mp
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a : α
l : List α
hel : x ∈ insert' a l
⊢ x = a ∨ x ∈ l