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)