[Agda] Need help completing a proof

[Philip Wadler]

I'm having trouble completing a proof, and would be grateful for help. The
problem arises because I need to show two values are equal, but the
equality of the values follows from a complex equation. In fact, it is not
hard to show that the equality follows from the equation, but when I
attempt to use the desired equality for rewriting Agda complains and I
can't work out what it is complaining about (or how to fix it).

A complete example is attached. The original is more complex, I've tried to
boil it down to its simplest form. My apologies that the simplest form is
not so simple!

Thank you for your help. Go well, -- P



.   \ Philip Wadler, Professor of Theoretical Computer Science,
.   /\ School of Informatics, University of Edinburgh
.  /  \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20211224/d112116a/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Example.lagda.md
Type: text/markdown
Size: 4567 bytes
Desc: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20211224/d112116a/attachment.bin>
-------------- next part --------------
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.