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