intro satDis
case mp
W : Type
l : List Formula
M : KripkeModel W
w : W
⊢ Evaluate (M, w) (bigDis l) → ∃ φ ∈ l, Evaluate (M, w) φ
case mp
W : Type
l : List Formula
M : KripkeModel W
w : W
satDis : Evaluate (M, w) (bigDis l)
⊢ ∃ φ ∈ l, Evaluate (M, w) φ