no goals
ι : Type ?u.106932
α : Type u_1
β : Type ?u.106938
inst✝¹ : Preorder α
inst✝ : Preorder β
s t : Set α
a : α
⊢ IsPwo (insert a s) ↔ IsPwo s
simp only [← singleton_union, isPwo_union, isPwo_singleton, true_and_iff]