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.
I tried avoiding that by using explicit `weaken`, as discussed, but the proofs seem to become more complicated (one just needs to apply `weaken-sound` in the right place and the right number of times). I'm ultimately comfortable with such a hack.