{P : Sort u} →
  {builtin : Std.HashMap Lean.Name (Array Lean.Meta.SimpTheoremKey)} →
    {newEntries : Lean.PHashMap Lean.Name (Array Lean.Meta.SimpTheoremKey)} →
      {builtin' : Std.HashMap Lean.Name (Array Lean.Meta.SimpTheoremKey)} →
        {newEntries' : Lean.PHashMap Lean.Name (Array Lean.Meta.SimpTheoremKey)} →
          { builtin := builtin, newEntries := newEntries } = { builtin := builtin', newEntries := newEntries' } →
            (builtin = builtin' → newEntries = newEntries' → P) → P