{P : Sort u} →
  {moduleName identName moduleName' identName' : String} →
    Lean.Lsp.RefIdent.const moduleName identName = Lean.Lsp.RefIdent.const moduleName' identName' →
      (moduleName = moduleName' → identName = identName' → P) → P