rw [conEval]
case cons.mpr.intro.intro.inl.h
W : Type
M : KripkeModel W
w : W
N : ℕ
XS : List (List Formula)
IH : evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
Y : List Formula
Ysat : ∀ f ∈ Y, evaluate M w f
⊢ evaluate M w (Con Y)
case cons.mpr.intro.intro.inl.h
W : Type
M : KripkeModel W
w : W
N : ℕ
XS : List (List Formula)
IH : evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
Y : List Formula
Ysat : ∀ f ∈ Y, evaluate M w f
⊢ ∀ f ∈ Y, evaluate M w f