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.
(Note to self: Turns out that diff-term & friends includes weakening, so it can take in the context arguments which are irrelevant, but then proving that [[ diff-term ]] environment1 == [[ diff-term ]] environment2, which is the problem I ran into, becomes harder; with weakening, that would be proven by weaken-sound).