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.