∀ {uri : Lean.Lsp.DocumentUri} {type : Lean.Lsp.FileChangeType} {uri_1 : Lean.Lsp.DocumentUri}
  {type_1 : Lean.Lsp.FileChangeType},
  { uri := uri, type := type } = { uri := uri_1, type := type_1 } → uri = uri_1 ∧ type = type_1