Yes, I am also suffering from it, but not often.<br><br>Best regards,<br>Dmytro <br><br><div class="gmail_quote">2013/1/24 Serge D. Mechveliani <span dir="ltr"><<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</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 Thu, Jan 24, 2013 at 04:50:59PM +0200, Dmytro Starosud wrote:<br>
> Ah, sorry, didn't notice that Level3 is tuple :)<br>
> For this you can use let-bindings:<br>
><br>
> \all {t : Level3} let (x , y , z) = t in (A : Set x) (B : Set y) ...<br>
><br>
<br>
</div>Yes. I have also discovered the possibility of this `let'.<br>
Initially, it was not parsed, because I have forgotten to import _,_<br>
<br>
(the report is only "cannot parse",<br>
and it is difficult to guess and recall of importing _,_).<br>
<br>
Thanks,<br>
<br>
------<br>
Sergei<br>
</blockquote></div><br>