induction' X with g X _
X : List Formula
f : Formula
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (Con (f :: X)) ↔ evaluate M w f ∧ evaluate M w (Con X)
case nil
f : Formula
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (Con [f]) ↔ evaluate M w f ∧ evaluate M w (Con [])

case cons
f : Formula
W : Type
M : KripkeModel W
w : W
g : Formula
X : List Formula
tail_ih✝ : evaluate M w (Con (f :: X)) ↔ evaluate M w f ∧ evaluate M w (Con X)
⊢ evaluate M w (Con (f :: g :: X)) ↔ evaluate M w f ∧ evaluate M w (Con (g :: X))