Compact representation for proofs

[fiedlr]

The slowness of our current implementation is, in a large part, due to the redundant proofs of lemmas (e.g. for lifting equivalences into contexts), storing proofs in their metamath representation, and keeping a large amount of unneeded lemmas in memory. We should instead be storing it as a direct representation of matching logic proofs, and only converting to metamath during serialization.

[nishantjr]

As a first step, we can use a compact internal representation, while still sticking with metamath.