more comments + rewriting list method
minor rewrite in axioms.t