rw [disconEval (XS ∪ YS) (by rfl)]
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)