Abstract out the proof verification process

[tirix]

One can imagine several clients/needs for an iteration through the proof tree, which follows the steps of the proof and accumulates on the stack:

• the proof verification itself,
• the translation into the ASCII typesetting - this can actually reuse the same method as the line above because
• the translation into the Unicode typesetting
• the translation into the STS typesetting - this requires Formulas on the stack
• an alternative proof verification mechanism, which could be entirely based on formulas. Substitutions and matching shall be very fast,
• one might also imaging a translation into a different proof language, a transformation or transposition of a proof which would apply some action on each of the step, e.g. an automatic transformation of an inductive proof into a deductive proof, or a transposition of a proof in the reals into the same proof in the general frame of ordered fields, or vice-versa, etc.

All these targets could be reached based on a single mechanism provided by the metamath-knife library. E.g. the client would provide an implementor of a given trait.

I've tried to implement this kind of abstraction in this PR, starting from proof.rs:

• ProofBuilder originally managed a stack of expressions as a u8 buffer. This PR introduces a generic type StackBuffer, implementing a new ProofStack trait for this.
• ProofBuilder originally managed expression being ranges over that buffer. This PR introduces a generic type Idx for that ProofStack, to address one element on the stack.
• Functions manipulating this stack (add_floating, add_essential, do_substitute, finish), etc. have been moved to default methods of the StackBuffer trait