intro satCon
case mp
W : Type
l : List Formula
M : KripkeModel W
w : W
⊢ Evaluate (M, w) (bigCon l) → ∀ φ ∈ l, Evaluate (M, w) φ
case mp
W : Type
l : List Formula
M : KripkeModel W
w : W
satCon : Evaluate (M, w) (bigCon l)
⊢ ∀ φ ∈ l, Evaluate (M, w) φ