simp
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
⊢ (∃ Y ∈ XS⊎YS, ∀ f ∈ Y, evaluate M w f) ↔ evaluate M w (discon XS⋀discon YS)
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) ↔
    evaluate M w (discon XS) ∧ evaluate M w (discon YS)