{P : Sort u} →
  {name : Aesop.RuleName} →
    {entries : Array Lean.Meta.SimpEntry} →
      {name' : Aesop.RuleName} →
        {entries' : Array Lean.Meta.SimpEntry} →
          { name := name, entries := entries } = { name := name', entries := entries' } →
            (name = name' → entries = entries' → P) → P