unfold semEquiv
XS YS : List (List Formula)
⊢ discon (XS⊎YS)≡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)