simp only [Formula.substPrime]
σ : Formula → Formula
V : VarBoolAssignment
a✝¹ : DefName
a✝ : List VarName
⊢ evalPrime V (substPrime σ (def_ a✝¹ a✝)) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) (def_ a✝¹ a✝)
σ : Formula → Formula
V : VarBoolAssignment
a✝¹ : DefName
a✝ : List VarName
⊢ evalPrime V (σ (def_ a✝¹ a✝)) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) (def_ a✝¹ a✝)