{P : Sort u} →
  {backend : Lean.Name} →
    {pattern : String} →
      {backend' : Lean.Name} →
        {pattern' : String} →
          Lean.ExternEntry.inline backend pattern = Lean.ExternEntry.inline backend' pattern' →
            (backend = backend' → pattern = pattern' → P) → P