This does seem to work, I have no idea why. I'm pretty sure there I've
made a mistake somewhere. Perhaps I shouldn't do equational reasoning
after just getting up, or just use Agda :-/
Congrats ! Vuvuzela !
If there are bugs in the proof, you can give it to your students to patch up.