Theorem: FOL.NV.is_tauto_def_false (FOL/NV/Margaris/Prop.lean)

State before:
⊢ (false_.iff_ true_.not_).IsTautoPrime
Tactic:
simp only [Formula.IsTautoPrime]
State after:
⊢ ∀ (V : VarBoolAssignment), evalPrime V (false_.iff_ true_.not_)

State before:
⊢ ∀ (V : VarBoolAssignment), evalPrime V (false_.iff_ true_.not_)
Tactic:
simp only [eval_not, eval_iff]
State after:
⊢ ∀ (V : VarBoolAssignment), evalPrime V false_ ↔ ¬evalPrime V true_

State before:
⊢ ∀ (V : VarBoolAssignment), evalPrime V false_ ↔ ¬evalPrime V true_
Tactic:
tauto
State after:
no goals