{P : Sort u} →
  {catName declName : Lean.Name} →
    {behavior : Lean.Parser.LeadingIdentBehavior} →
      {catName' declName' : Lean.Name} →
        {behavior' : Lean.Parser.LeadingIdentBehavior} →
          Lean.Parser.ParserExtension.OLeanEntry.category catName declName behavior =
              Lean.Parser.ParserExtension.OLeanEntry.category catName' declName' behavior' →
            (catName = catName' → declName = declName' → behavior = behavior' → P) → P