simp only [evalPrime_substPrime_eq_evalPrime_evalPrime P σ 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 (fun H => decide (evalPrime V (σ H))) P