proofs on parsing and printing of primitives and macro

Currently when a new type or instruction is added to the typed syntax, it is not possible to forget to add it to the untyped syntax and to adapt the elaboration pass to take it into account because not doing so breaks the proofs in untyper.v. This MR is about extending this to the next level to make it impossible to forget to update the pretty-printer, the parser, and the macro expansion steps. This also improves the guarantees we have on these tricky functions; in particular by proving that what gets out of the pretty-printer can always be correctly understood by the parser.