Changes

Summary

1. more operations: zterm ordering that follows fast_term_ord;
2. clarified signature; clarified modules;
3. clarified modules;
4. more zproofs;
5. more zproofs, imitating existing proofs (which are a bit rough here);
6. tuned signature;
7. tuned whitespace;
8. minor performance tuning;