rw [disconEval (XS ∪ YS)]
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (discon (XS ∪ YS)) ↔ evaluate M w (discon XS⋁discon YS)
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)