specialize h1 V
case h2.h3
P : Formula
h1 : ∀ (V : VarBoolAssignment), evalPrime V P
V : VarBoolAssignment
⊢ P = if evalPrime V P then P else P.not_
case h2.h3
P : Formula
V : VarBoolAssignment
h1 : evalPrime V P
⊢ P = if evalPrime V P then P else P.not_