[Agda] trivial lemma of `with'

[Sergei Meshveliani]

On Fri, 2014-01-03 at 18:25 +0100, Andreas Abel wrote:
> Irrelevant arguments (a bit unluckily marked by a dot) can only be used 
> in irrelevant positions.  Thus, if you want to use _divMod_ of the 
> std-lib, you will run into trouble (as you describe below).
> 
> Nisse does not make use of irrelevance, so there are no uses of it in 
> the standard library.

The thing is so important that, probably, it needs to become a part of
the (future) Agda standard.
Without the irrelevance annotation many proofs will be difficult to
write.

> As an alternative to irrelevance, you can claim proof irrelevance 
> manually, e.g. by adding a field
> 
>    dRemIrr : (x y : C) (p q : \neg (y \approx 0#)) ->
>      dRem x y p == dRem x y q
> 
> for a suitable notion of equality ==.
> 
> Then, of course, you have to prove it for each instance of Foo.


But this relies on  _==_.

(I suspect that I misuse irrelevance in my examples in the Bug tracker
1013).

My real application has 

   divRem  : (x y : C) → .(nz : y ≉ 0#) → DivRem eucNorm x y _,      (1)

where  DivRem  is a certain record, and these records are not at all
expected to be compared for equality.

What kind of irrelevance means this   .(nz : y ≉ 0#)
?
I find the 'Irrelevance' topic in the online manual.
And it is not clear from it of whether the usage (1) of irrelevance is
correct. The manual says in the beginning  
             "... f  does not depend computationally on its argument".

What kind of _==_ is presumed in this sentence?

Thanks,

------
Sergei