case not_ phi phi_ih =>
  simp only [Formula.primeSet] at h1
  simp only [evalPrimeFfToNot] at phi_ih
  simp only [evalPrimeFfToNot]
  simp only [evalPrime]
  simp
  split_ifs
  case _ c1 =>
    simp only [c1] at phi_ih
    simp at phi_ih
    apply IsDeduct.mp_ phi
    apply proof_imp_deduct
    apply T_14_6
    exact phi_ih h1
  case _ c1 =>
    simp only [c1] at phi_ih
    simp at phi_ih
    exact phi_ih 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_)
no goals