case
    imp_ phi psi phi_ih psi_ih
  | and_ phi psi phi_ih psi_ih
  | or_ phi psi phi_ih psi_ih
  | iff_ phi psi phi_ih psi_ih =>
  simp only [Formula.substPrime]
  simp only [Formula.evalPrime]
  congr! 1
σ : 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)
no goals