<br><br><div class="gmail_quote">On Thu, Jan 28, 2010 at 4:19 PM, Ruben Henner Zilibowitz <span dir="ltr">&lt;<a href="mailto:rzilibowitz@yahoo.com.au">rzilibowitz@yahoo.com.au</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
<div style="word-wrap:break-word"><div>Ok. Thanks. Now how do I write this function?</div><div></div></div></blockquote><div> </div><div>∣∣-pres-≡ : {x y : ℤ} → x ≡ y → ∣ x ∣ ≡ ∣ y ∣</div><div>∣∣-pres-≡ refl = refl</div><div>
<br></div><div>/ Ulf</div></div>