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)
      (match head :: tail with
      | [] => ⊤
      | [f] => f
      | f :: rest => f⋀bigCon rest) ↔
    Evaluate (M, w) head ∧
      Evaluate (M, w)
        (match tail with
        | [] => ⊤
        | [f] => f
        | f :: rest => f⋀bigCon rest)
no goals