{P : Sort u} →
  {shortName declName : Lean.Name} →
    {levelNames : List Lean.Name} →
      {docString? : Option (Lean.TSyntax `Lean.Parser.Command.docComment × Bool)} →
        {shortName' declName' : Lean.Name} →
          {levelNames' : List Lean.Name} →
            {docString?' : Option (Lean.TSyntax `Lean.Parser.Command.docComment × Bool)} →
              { shortName := shortName, declName := declName, levelNames := levelNames, docString? := docString? } =
                  { shortName := shortName', declName := declName', levelNames := levelNames',
                    docString? := docString?' } →
                (shortName = shortName' →
                    declName = declName' → levelNames = levelNames' → docString? = docString?' → P) →
                  P