{P : Sort u} →
  {uri : Lean.Lsp.DocumentUri} →
    {sessionId : UInt64} →
      {uri' : Lean.Lsp.DocumentUri} →
        {sessionId' : UInt64} →
          { uri := uri, sessionId := sessionId } = { uri := uri', sessionId := sessionId' } →
            (uri = uri' → sessionId = sessionId' → P) → P