have : ((Evaluate (M, w) head) ∧ Evaluate (M, w) (bigCon tail)) :=
  by unfold bigCon; aesop
W : Type
M : KripkeModel W
w : W
head : Formula
tail : List Formula
ih : Evaluate (M, w) (bigCon tail) → ∀ φ ∈ tail, Evaluate (M, w) φ
satCon : Evaluate (M, w) (bigCon (head :: tail))
⊢ ∀ φ ∈ head :: tail, Evaluate (M, w) φ
W : Type
M : KripkeModel W
w : W
head : Formula
tail : List Formula
ih : Evaluate (M, w) (bigCon tail) → ∀ φ ∈ tail, Evaluate (M, w) φ
satCon : Evaluate (M, w) (bigCon (head :: tail))
this : Evaluate (M, w) head ∧ Evaluate (M, w) (bigCon tail)
⊢ ∀ φ ∈ head :: tail, Evaluate (M, w) φ