case forall_ x phi phi_ih =>
  let F := forall_ x phi
  simp only [Formula.primeSet] at h1
  simp at h1
  simp only [evalPrimeFfToNot]
  simp only [Formula.evalPrime]
  apply IsDeduct.assume_
  simp
  apply Exists.intro F
  tauto
Δ_U : Set Formula
V : VarBoolAssignment
x : VarName
phi : Formula
phi_ih : ↑phi.primeSet ⊆ Δ_U → IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V phi)
h1 : ↑(forall_ x phi).primeSet ⊆ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (forall_ x phi))
no goals