case eq_ x y =>
  let F := eq_ x y
  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 y : VarName
h1 : ↑(eq_ x y).primeSet ⊆ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (eq_ x y))
no goals