no goals
α : Type u_1
β : Type ?u.23072
γ : Type ?u.23075
δ : Type ?u.23078
δ' : Type ?u.23081
ι : Sort ?u.23084
s✝ t u s : Set α
⊢ ∀ (s : Set α), (fun s => s = ∅ ∨ s = univ) s → (fun s => s = ∅ ∨ s = univ) (sᶜ)
simp (config := { contextual := true }) [or_imp]