Theorem: evalDis (Bml/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