assumption
case cons
W : Type
M : KripkeModel W
w : W
f : Formula
X : List Formula
IH : Evaluate (M, w) (bigCon X) ↔ ∀ f ∈ X, Evaluate (M, w) f
a✝ : Evaluate (M, w) f
⊢ Evaluate (M, w) (bigCon X) ↔ ∀ a ∈ X, Evaluate (M, w) a
no goals