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

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

State before:
⊢ ∀ (V : VarBoolAssignment), evalPrime V true_
Tactic:
simp only [Formula.evalPrime]
State after:
⊢ VarBoolAssignment → True

State before:
⊢ VarBoolAssignment → True
Tactic:
simp
State after:
no goals