intro W M w
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
⊢ Evaluate (M, w) (discon (XS⊎YS)) ↔ Evaluate (M, w) (discon XS⋀discon YS)