case cons head tail ih =>
  have : Evaluate (M, w) (bigCon (head :: tail)) ↔
    ((Evaluate (M, w) head) ∧ Evaluate (M, w) (bigCon tail)) :=
    by unfold bigCon; aesop
  aesop
W : Type
M : KripkeModel W
w : W
head : Formula
tail : List Formula
ih : (∀ φ ∈ tail, Evaluate (M, w) φ) → Evaluate (M, w) (bigCon tail)
satAll : ∀ φ ∈ head :: tail, Evaluate (M, w) φ
⊢ Evaluate (M, w) (bigCon (head :: tail))
no goals