[Agda] Erasable vs. irrelevant, and red black trees again

[jleivent at comcast.net]

>> Thus, I think Jonathan's trick has some right of existence.
>
>I wouldn't disagree.

Wow.  Erasable encouragement.

Anyway, I do think this trick can be generalized.

-- Jonathan Leivent