aesop
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
⊢ (∃ a ∈ XS, ∃ b ∈ YS, ∀ (f : Formula), f ∈ a ∨ f ∈ b → Evaluate (M, w) f) ↔
    (∃ Y ∈ XS, ∀ f ∈ Y, Evaluate (M, w) f) ∧ ∃ Y ∈ YS, ∀ f ∈ Y, Evaluate (M, w) f
no goals