simp
case cons
W : Type
M : KripkeModel W
w : W
f : Formula
X : List Formula
IH : evaluate M w (Con X) ↔ ∀ f ∈ X, evaluate M w f
⊢ evaluate M w f ∧ evaluate M w (Con X) ↔ ∀ f_1 ∈ f :: X, evaluate M w f_1
case cons
W : Type
M : KripkeModel W
w : W
f : Formula
X : List Formula
IH : evaluate M w (Con X) ↔ ∀ f ∈ X, evaluate M w f
⊢ evaluate M w f → (evaluate M w (Con X) ↔ ∀ a ∈ X, evaluate M w a)