Make _⊕_ more coherent with _⊝_
Fixup old comments
Add extension points for nil primitive

This commit adds nil to the basic operations of the plugin interface,
like apply and diff.

This implies adding various other related components, and adding
implementations for Nehemiah.

This operation is not yet used anywhere - in particular, the algebra of
changes still has a fixed definition, so proofs need not be
altered *yet*.

More extension points will be added later.
Reorder primitives: 1st apply, 2nd diff, 3rd nil

Sometimes, diff came before apply - which is inconsistent with most
other modules and the expected order (the usual order of operations is
+, -). Moreover, nil makes most sense next to diff, since nil v is
equivalent to diff v v (with a possibly better implementation).
More extension points for proof plugin
Stop assuming nil v is v ⊟ v
Make nil an extension point in change algebra

This defines nil changes for groups as their identity element, and
updates nil changes also for Nehemiah (since this plugin uses group
changes for its base types).