<div dir="ltr">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).<div><br></div><div>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!<br><div><br></div><div>Thank you for your help. Go well, -- P<br><div><br></div><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></div>