[Axiom-developer] Proving Axiom Correct

[daly]

The latest push extracts the functions from the algebra as preparation
for COQ proofs. There is still work to be done to decorate the functions
in domains and packages with their signatures which is the next thing
to pursue.

All of these functions are collected into obj/sys/proofs/coq.v if
the make command line includes COQ=coq, otherwise the extraction
step is ignored. The coq.v file is pushed through coqtop to rerun
any proofs. At the moment all of the functions are comments.

Part of the game is to prove the most primitive functions first.
This has two advantages. First, the proofs can be used during more
complex proofs. Second, a lot of the primitive functions are just
calls to the underlying lisp code.

The underlying lisp code is being proven using ACL2 (also against
auto-extracted code chunks) so there is a nice focus on a small
set of primitives that benefit both the lisp- and spad-level code.

Tim