Add extension points for nil

I finally allowed plugins to customize the definition of nil.
The changes are less scary than I expected.

If you want to review this, an interesting question is naming for the various ops corresponding to nil.
With the current convensions, I should use a boxed 0, a circled 0 and a circled 0 in semantic brackets, but I didn't find the first two characters right away by \0.

Right now, they're respectively nil (the semantic op in the change algebra), nilt for the corresponding term, and nil in semantic brackets for the semantic operation corresponding to the term.
Candidates for nil are indeed delta-equivalent, by `update-diff` and `update-nil` (used in `⊞-unit-is-nil`).