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

State before:
P Q : Formula
V : VarBoolAssignment
⊢ evalPrime V (P.iff_ Q) ↔ (evalPrime V P ↔ evalPrime V Q)
Tactic:
simp only [Formula.evalPrime]
State after:
no goals