{P : Sort u} →
  {tree : Lean.Meta.DiscrTree Mathlib.Meta.NormNum.NormNumExt} →
    {erased : Lean.PHashSet Lean.Name} →
      {tree' : Lean.Meta.DiscrTree Mathlib.Meta.NormNum.NormNumExt} →
        {erased' : Lean.PHashSet Lean.Name} →
          { tree := tree, erased := erased } = { tree := tree', erased := erased' } →
            (tree = tree' → erased = erased' → P) → P