simp only [Formula.substPrime]
σ : Formula → Formula
V : VarBoolAssignment
phi psi : Formula
phi_ih : evalPrime V (substPrime σ phi) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) phi
psi_ih : evalPrime V (substPrime σ psi) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) psi
⊢ evalPrime V (substPrime σ (phi.iff_ psi)) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) (phi.iff_ psi)
σ : Formula → Formula
V : VarBoolAssignment
phi psi : Formula
phi_ih : evalPrime V (substPrime σ phi) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) phi
psi_ih : evalPrime V (substPrime σ psi) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) psi
⊢ evalPrime V ((substPrime σ phi).iff_ (substPrime σ psi)) ↔
    evalPrime (fun H => decide (evalPrime V (σ H))) (phi.iff_ psi)