cases' XS with X XS
W : Type
M : KripkeModel W
w : W
N : ℕ
XS : List (List Formula)
IH :
  ∀ m < XS.length,
    ∀ (XS : List (List Formula)), XS.length = m → (Evaluate (M, w) (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, Evaluate (M, w) f)
⊢ Evaluate (M, w) (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, Evaluate (M, w) f
case nil
W : Type
M : KripkeModel W
w : W
N : ℕ
IH :
  ∀ m < [].length,
    ∀ (XS : List (List Formula)), XS.length = m → (Evaluate (M, w) (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, Evaluate (M, w) f)
⊢ Evaluate (M, w) (discon []) ↔ ∃ Y ∈ [], ∀ f ∈ Y, Evaluate (M, w) f

case cons
W : Type
M : KripkeModel W
w : W
N : ℕ
X : List Formula
XS : List (List Formula)
IH :
  ∀ m < (X :: XS).length,
    ∀ (XS : List (List Formula)), XS.length = m → (Evaluate (M, w) (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, Evaluate (M, w) f)
⊢ Evaluate (M, w) (discon (X :: XS)) ↔ ∃ Y ∈ X :: XS, ∀ f ∈ Y, Evaluate (M, w) f