∀ {pre post : Bool}
  {eval : {u : Lean.Level} → {α : Q(Type u)} → (e : Q(«$α»)) → Lean.MetaM (Mathlib.Meta.NormNum.Result e)}
  {name : autoParam Lean.Name Mathlib.Meta.NormNum.NormNumExt.name._autoParam} {pre_1 post_1 : Bool}
  {eval_1 : {u : Lean.Level} → {α : Q(Type u)} → (e : Q(«$α»)) → Lean.MetaM (Mathlib.Meta.NormNum.Result e)}
  {name_1 : autoParam Lean.Name Mathlib.Meta.NormNum.NormNumExt.name._autoParam},
  { pre := pre, post := post, eval := eval, name := name } =
      { pre := pre_1, post := post_1, eval := eval_1, name := name_1 } →
    pre = pre_1 ∧ post = post_1 ∧ eval = eval_1 ∧ name = name_1