simp at Y_in
case cons.mpr.intro.intro
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
Y : List Formula
Y_in : Y ∈ X :: XS
Ysat : ∀ f ∈ Y, Evaluate (M, w) f
⊢ Evaluate (M, w) (bigCon X) ∨ ∃ Y ∈ XS, ∀ f ∈ Y, Evaluate (M, w) f
case cons.mpr.intro.intro
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
Y : List Formula
Ysat : ∀ f ∈ Y, Evaluate (M, w) f
Y_in : Y = X ∨ Y ∈ XS
⊢ Evaluate (M, w) (bigCon X) ∨ ∃ Y ∈ XS, ∀ f ∈ Y, Evaluate (M, w) f