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)