constructor
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
⊢ Evaluate (M, w) (bigDis l) → ∃ φ ∈ l, Evaluate (M, w) φ

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