WIP: use bytes to represent identifiers in the proofmode

In order to make proof terms more compact, we use list byte for identifiers where byte is an inductive with 256 constructors, rather than String.string which is based on Ascii.ascii, a record of 8 booleans.

This crucially relies on a feature of Coq v8.11 to add new string printing types, since otherwise IPM contexts will not be printed with human-readable strings using only notations.

There is one really annoying backwards incompatibility I need to fix: formerly a coercion from strings to identifiers allowed a bunch of code to mostly ignore the difference between a named identifier and a string. The coercion from bytes to identifiers works the same way still, but a new coercion from strings to bytes doesn't get triggered correctly without importing it directly. This is probably a Coq bug that needs to be reported and then we need a workaround (eg, it seems like exporting the declaration of the coercion might work, which we can do if it's in a separate module).

Making Perennial compatible with this wasn't straightforward, because of the bug above combined with the fact that occasionally do low-level things with identifiers for custom proof mode tactics. It was also only 3% faster (4025 vs 4163 total CPU seconds), which implies this isn't worth it.