Implemented --total flag (very experimental)

--total enables some transformations that assume totality.
I expect more bugs, especially linked with caching of
defining hyperedges.
Addition associativity can't be proved yet because
eqprover refuses to prove that the node is equivalent
to itself (but with a nontrivial renaming). But still
we can prove all required lemmas.