simp only [Formula.primeSet] at h1
Δ_U : Set Formula
V : VarBoolAssignment
X : DefName
xs : List VarName
h1 : ↑(def_ X xs).primeSet ⊆ Δ_U
F : Formula := def_ X xs
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (def_ X xs))
Δ_U : Set Formula
V : VarBoolAssignment
X : DefName
xs : List VarName
h1 : ↑{def_ X xs} ⊆ Δ_U
F : Formula := def_ X xs
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (def_ X xs))