<div dir="ltr">On Wed, Sep 9, 2015 at 3:24 PM, Jonas Scholl <span dir="ltr"><<a href="mailto:anselm.scholl@tu-harburg.de" target="_blank">anselm.scholl@tu-harburg.de</a>></span> wrote:<br><div class="gmail_extra"><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">How about trying to prove the following:<br>
<br>
mac (compile e ++ x) s = mac x (eval e : s)<br>
<br>
You can then just break down your term into pieces, build up the stack<br>
and evaluate it in your prove.<br></blockquote><div><br></div><div><br>Thanks Jonas, Janis<br></div><div>I knew I had to generalize it but not in '2 dimensions' -- x and s !<br></div><div>Seems obvious on further reflection<br></div><div>I wonder though what is the moral for formulating theorems of right generality?<br></div><div><br></div></div>
</div></div>