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