no goals
α : Type u_1
β : Type ?u.22240
γ : Type ?u.22243
δ : Type ?u.22246
δ' : Type ?u.22249
ι : Sort ?u.22252
s t u : Set α
S : Set (Set α)
⊢ generateFrom (insert univ S) = generateFrom S
rw [insert_eq, ← generateFrom_sup_generateFrom, generateFrom_singleton_univ, bot_sup_eq]