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)