rw [insert', List.mem_singleton]
case mpr.nil
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a : α
hor : x = a ∨ x ∈ []
⊢ x ∈ insert' a []
case mpr.nil
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a : α
hor : x = a ∨ x ∈ []
⊢ x = a