subst h3
F F' : Formula
Δ_U : Set Formula
V : VarBoolAssignment
h1 : ↑F.primeSet ⊆ Δ_U
h3 : F' = evalPrimeFfToNot V F
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) F'
F : Formula
Δ_U : Set Formula
V : VarBoolAssignment
h1 : ↑F.primeSet ⊆ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V F)