∀ {stx : Lean.Syntax} {type : Lean.Lsp.SemanticTokenType} {priority : ℕ} {stx_1 : Lean.Syntax}
  {type_1 : Lean.Lsp.SemanticTokenType} {priority_1 : ℕ},
  { stx := stx, type := type, priority := priority } = { stx := stx_1, type := type_1, priority := priority_1 } →
    stx = stx_1 ∧ type = type_1 ∧ priority = priority_1