case pred_const_ | pred_var_ | eq_ | forall_ | exists_ | def_ =>
  simp only [Formula.substPrime]
  simp only [Formula.evalPrime]
  simp
σ : 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✝)
no goals