∀ {kind : Lean.SyntaxNodeKind} {type? : Option Std.Format} {kind_1 : Lean.SyntaxNodeKind} {type?_1 : Option Std.Format},
  Lean.Doc.DocHighlight.literal kind type? = Lean.Doc.DocHighlight.literal kind_1 type?_1 →
    kind = kind_1 ∧ type? = type?_1