WIP: Port proofmode to use more efficient bytes type

I started working on #317.

The proof mode and its tests pass, but heap lang is broken. There's one serious downside to the implementation: in order to get strings passed to tactics to parse as bytes, the default string interpretation has to be bytes, rather than carefully using the new bytes_scope where a proof mode string is expected. This breaks heap lang binders.

A more conservative implementation would continue to parse everything as strings but use bytes internally; this would incur the cost of some conversions whenever identifiers are first passed from the user, but terms would be more compact from then on.

This whole change only improves performance by making terms more compact, so it's somewhat unclear to me how worthwhile it is. One test I would do to evaluate this is to make identifiers much larger, say by just using long names, and see if that really hurts performance much.