rw [disconEval YS (by rfl)]
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
⊢ (∃ Y, (Y ∈ XS ∨ Y ∈ YS) ∧ ∀ f ∈ Y, Evaluate (M, w) f) ↔
    (¬∃ Y ∈ XS, ∀ f ∈ Y, Evaluate (M, w) f) → Evaluate (M, w) (discon YS)
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
⊢ (∃ Y, (Y ∈ XS ∨ Y ∈ YS) ∧ ∀ f ∈ Y, Evaluate (M, w) f) ↔
    (¬∃ Y ∈ XS, ∀ f ∈ Y, Evaluate (M, w) f) → ∃ Y ∈ YS, ∀ f ∈ Y, Evaluate (M, w) f