no goals
ι : Type ?u.107703
α : Type u_1
β : Type ?u.107709
inst✝¹ : Preorder α
inst✝ : Preorder β
s t : Set α
a : α
⊢ IsWf (insert a s) ↔ IsWf s
simp only [← singleton_union, isWf_union, isWf_singleton, true_and_iff]