Theorem: evalDis (Pdl/Semantics.lean)

State before:
W : Type
M : KripkeModel W
f g : Formula
w : W
⊢ evaluate M w (f⋁g) ↔ evaluate M w f ∨ evaluate M w g
Tactic:
simp
State after:
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

State before:
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
Tactic:
tauto
State after:
no goals