no goals
ι : Type ?u.108524
α : Type u_1
β : Type ?u.108530
r : α → α → Prop
inst✝ : IsStrictOrder α r
s : Set α
a : α
⊢ WellFoundedOn (insert a s) r ↔ WellFoundedOn s r
simp only [← singleton_union, wellFoundedOn_union, wellFoundedOn_singleton, true_and_iff]