Do you mean something like this? <br><pre><a href="http://publications.lib.chalmers.se/records/fulltext/146810.pdf,">http://publications.lib.chalmers.se/records/fulltext/146810.pdf</a></pre>Thanks,<br>Dmytro <br><br><br><div class="gmail_quote">
2013/2/4 Nils Anders Danielsson <span dir="ltr"><<a href="mailto:nad@chalmers.se" target="_blank">nad@chalmers.se</a>></span><br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div class="im">On 2013-02-01 22:35, Dmytro Starosud wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Is there any way to substitute "f refl" with some "g"?<br>
</blockquote>
<br></div>
One option, that may or may not work for you, is to switch from Set to a<br>
universe for which a conservative approximation of equality is<br>
decidable. Then you can use an implicit argument of type<br>
<br>
True ("decision procedure says yes").<span class="HOEnZb"><font color="#888888"><br>
<br>
-- <br>
/NAD<br>
</font></span></blockquote></div><br>