Make _⊕_ more coherent with _⊝_
Fixup old comments
Reorder primitives: 1st apply, 2nd diff

Sometimes, diff came before apply - which is inconsistent with most
other modules and the expected order (the usual order of operations is
+, -). Moreover, later we'll add nil last, and that makes most sense
next to diff, since nil v is equivalent to diff v v (with a possibly
better implementation).
Cleanup
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.
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).