rw [disconEval XS]
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
⊢ (∃ Y, (Y ∈ XS ∨ Y ∈ YS) ∧ ∀ f ∈ Y, evaluate M w f) ↔ ¬evaluate M w (discon XS) → 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) → evaluate M w (discon YS)