<div dir="ltr"><blockquote style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex" class="gmail_quote">I'm happy to make a minor tweak to the definition of st2heap and prove<br>
the following. I would appreciate help with proving lemma 2 from the<br>
following.</blockquote><div class="gmail_extra"><br></div><div class="gmail_extra">No problem. I've replaced my cheated lemma 2 by the one you said you'd provide (i.e. I proved what I need from that).<br></div><div class="gmail_extra"><br><div class="gmail_quote">On 7 October 2016 at 22:06, Armaël Guéneau <span dir="ltr"><<a href="mailto:armael.gueneau@ens-lyon.fr" target="_blank">armael.gueneau@ens-lyon.fr</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class=""><br>
<br>
On 07/10/2016 12:39, Magnus Myreen wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Excellent!<br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
I have proved the following connection between CF's app_basic (as on master) and a revised formulation of the translator's Arrow, modulo 4 cheats. In this email, I will show: the final theorem proved, the cheated lemmas, and the new Arrow definition. I ask for the following feedback:<br>
1. Does the final theorem look like a strong enough connection?<br>
</blockquote>
Probably yes. I think Armaël might know better than me.<br>
</blockquote></span>
Yes, I think it's strong enough.<br>
<br>
</blockquote></div><br></div></div>