cases' XS with Y YS
X : List Formula
XS : List (List Formula)
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (discon (X :: XS)) ↔ evaluate M w (Con X⋁discon XS)
case nil
X : List Formula
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (discon [X]) ↔ evaluate M w (Con X⋁discon [])

case cons
X : List Formula
W : Type
M : KripkeModel W
w : W
Y : List Formula
YS : List (List Formula)
⊢ evaluate M w (discon (X :: Y :: YS)) ↔ evaluate M w (Con X⋁discon (Y :: YS))