It would be nice if proof assistants supported custom LSP semantic highlighting annotations on definitions/postulates. It would really level up embedded DSLs.