no goals
α : Type u_1
β : Type ?u.22617
γ : Type ?u.22620
δ : Type ?u.22623
δ' : Type ?u.22626
ι : Sort ?u.22629
s t u : Set α
S : Set (Set α)
⊢ generateFrom (insert ∅ S) = generateFrom S
rw [insert_eq, ← generateFrom_sup_generateFrom, generateFrom_singleton_empty, bot_sup_eq]