simp only [Formula.primeSet] at h1
Δ_U : Set Formula
V : VarBoolAssignment
phi : Formula
phi_ih : ↑phi.primeSet ⊆ Δ_U → IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V phi)
h1 : ↑phi.not_.primeSet ⊆ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V phi.not_)
Δ_U : Set Formula
V : VarBoolAssignment
phi : Formula
phi_ih : ↑phi.primeSet ⊆ Δ_U → IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V phi)
h1 : ↑phi.primeSet ⊆ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V phi.not_)