<div dir="ltr"><div class="gmail_extra"><br><div class="gmail_quote">On 24 October 2013 14:15, Sergei Meshveliani <span dir="ltr">&lt;<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>&gt;</span> wrote:<br>


<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div style="overflow:hidden">I manage to build a value in  A ⇔ B  by applying the function  Equiv.equivalence.<br>



But, for example, having<br>
                  e  :  m≤n ⇔ suc-m≤suc-n<br>
<br>
how to extract    to :  m ≤ n → suc m ≤ suc n<br>
from  e  ?</div></blockquote></div><br></div><div class="gmail_extra">Using auto (C-c C-a) I got:<br><br>open import Function.Equivalence<br>open import Function.Equality<br><br>foo : {A B : Set} → A ⇔ B → A → B<br>foo h = _⟨$⟩_ (Equivalence.to h)<br>


<br>-- <br>Andrés<br>
</div></div>