{P : Sort u} →
  {uri : Lean.Lsp.DocumentUri} →
    {version? : Option ℕ} →
      {uri' : Lean.Lsp.DocumentUri} →
        {version?' : Option ℕ} →
          { uri := uri, version? := version? } = { uri := uri', version? := version?' } →
            (uri = uri' → version? = version?' → P) → P