rw [conEval] at lhs
case h
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
lhs : Evaluate (M, w) (bigCon X)
⊢ ∀ f ∈ X, Evaluate (M, w) f
case h
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
lhs : ∀ f ∈ X, Evaluate (M, w) f
⊢ ∀ f ∈ X, Evaluate (M, w) f