case false_ =>
  simp only [Formula.primeSet] at h1
  simp at h1
  simp only [evalPrimeFfToNot]
  simp only [Formula.evalPrime]
  simp
  sorry
Δ_U : Set Formula
V : VarBoolAssignment
h1 : ↑false_.primeSet ⊆ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V false_)
no goals