no goals
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s✝ t : Set α
a✝ b : α
inst✝ : SemilatticeSup γ
a : γ
s : Set γ
⊢ BddAbove (insert a s) ↔ BddAbove s
simp only [insert_eq, bddAbove_union, bddAbove_singleton, true_and_iff]