[Agda] More rewrite woes

[Philip Wadler]

I've attached code where a rewrite should work but does not. There are many
places in the full development where I encounter similar issues. Rewrite
works fine in the original definition of left-id, but not in the subsequent
attempt to prove reflᴹ. Any advice on how to fix it?

The file is cut down from the original---I apologise that it is still
rather lengthy. The issue with rewrite appears at the end. I am using Agda
version 2.6.1.1-fce01db.

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/20220109/975f9c27/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: LeftId.lagda.md
Type: text/markdown
Size: 9367 bytes
Desc: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20220109/975f9c27/attachment.bin>
-------------- next part --------------
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.