<div dir="ltr">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?<div><br></div><div>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.</div><div><br></div><div>Thank you for your help! Go well, -- P</div><div><br></div><div><br><div><br></div><div><br clear="all"><div><div dir="ltr" class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div><div dir="ltr"><div dir="ltr"><div><div dir="ltr">.   \ Philip Wadler, Professor of Theoretical Computer Science,<br>.   /\ School of Informatics, University of Edinburgh<br></div><div>.  /  \ and Senior Research Fellow, IOHK<br></div><div dir="ltr">. <span><a href="http://homepages.inf.ed.ac.uk/wadler/" target="_blank">http://homepages.inf.ed.ac.uk/wadler/</a></span></div></div><div dir="ltr"><br></div></div></div></div></div></div></div></div></div></div>