subst a2
case h.true
U : Formula
Δ : Set Formula
V : VarBoolAssignment
h1_U : U.IsPrime
h2 : U ∉ Δ
U' : Formula
a1 : U' ∈ Δ
h1_Δ : U'.IsPrime
a2 : U' = U
⊢ U' = evalPrimeFfToNot V U'
case h.true
Δ : Set Formula
V : VarBoolAssignment
U' : Formula
a1 : U' ∈ Δ
h1_Δ h1_U : U'.IsPrime
h2 : U' ∉ Δ
⊢ U' = evalPrimeFfToNot V U'