induction l
case mpr
W : Type
l : List Formula
M : KripkeModel W
w : W
satAll : ∀ φ ∈ l, Evaluate (M, w) φ
⊢ Evaluate (M, w) (bigCon l)
case mpr.nil
W : Type
M : KripkeModel W
w : W
satAll : ∀ φ ∈ [], Evaluate (M, w) φ
⊢ Evaluate (M, w) (bigCon [])

case mpr.cons
W : Type
M : KripkeModel W
w : W
head✝ : Formula
tail✝ : List Formula
tail_ih✝ : (∀ φ ∈ tail✝, Evaluate (M, w) φ) → Evaluate (M, w) (bigCon tail✝)
satAll : ∀ φ ∈ head✝ :: tail✝, Evaluate (M, w) φ
⊢ Evaluate (M, w) (bigCon (head✝ :: tail✝))