unfold semEquiv
X : List Formula
⊢ ∀ (XS : List (List Formula)), discon (X :: XS)≡Con X⋁discon XS
X : List Formula
⊢ ∀ (XS : List (List Formula)) (W : Type) (M : KripkeModel W) (w : W),
    evaluate M w (discon (X :: XS)) ↔ evaluate M w (Con X⋁discon XS)