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