simp only [evalPrimeFfToNot] at phi_ih
Δ_U : Set Formula
V : VarBoolAssignment
phi psi : Formula
phi_ih : ↑phi.primeSet ⊆ Δ_U → IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V phi)
psi_ih : ↑psi.primeSet ⊆ Δ_U → IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V psi)
h1 : ↑phi.primeSet ⊆ Δ_U ∧ ↑psi.primeSet ⊆ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (phi.imp_ psi))
Δ_U : Set Formula
V : VarBoolAssignment
phi psi : Formula
psi_ih : ↑psi.primeSet ⊆ Δ_U → IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V psi)
h1 : ↑phi.primeSet ⊆ Δ_U ∧ ↑psi.primeSet ⊆ Δ_U
phi_ih :
  ↑phi.primeSet ⊆ Δ_U →
    IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (if evalPrime V phi then phi else phi.not_)
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (phi.imp_ psi))