simp
W : Type
M : KripkeModel W
f g : Formula
w : W
⊢ Evaluate (M, w) (f⋁g) ↔ Evaluate (M, w) f ∨ Evaluate (M, w) g
W : Type
M : KripkeModel W
f g : Formula
w : W
⊢ ¬Evaluate (M, w) f → Evaluate (M, w) g ↔ Evaluate (M, w) f ∨ Evaluate (M, w) g