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) φ
this : Evaluate (M, w) (bigCon (head :: tail)) ↔ Evaluate (M, w) head ∧ Evaluate (M, w) (bigCon tail)
⊢ Evaluate (M, w) (bigCon (head :: tail))
no goals