intro V
P : Formula
h1 : ∀ (V : VarBoolAssignment), evalPrime V P
σ : Formula → Formula
⊢ ∀ (V : VarBoolAssignment), evalPrime V (substPrime σ P)
P : Formula
h1 : ∀ (V : VarBoolAssignment), evalPrime V P
σ : Formula → Formula
V : VarBoolAssignment
⊢ evalPrime V (substPrime σ P)