rw [disconEvalHT]
case cons
W : Type
M : KripkeModel W
w : W
N : ℕ
X : List Formula
XS : List (List Formula)
IH : evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
⊢ evaluate M w (discon (X :: XS)) ↔ ∃ Y ∈ X :: XS, ∀ f ∈ Y, evaluate M w f
case cons
W : Type
M : KripkeModel W
w : W
N : ℕ
X : List Formula
XS : List (List Formula)
IH : evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
⊢ evaluate M w (Con X⋁discon XS) ↔ ∃ Y ∈ X :: XS, ∀ f ∈ Y, evaluate M w f