[Agda] y ≟ 0 for irrelevant y ≉ 0

[Sergei Meshveliani]

People,

I have a code like

  -- (I)
  eucQuot' : (x y : C) → (nz : y ≉ 0#) → C
  eucQuot' x y _ =  quot $ divRem x y _

  lemma : {x y : C} → (nz : y ≉ 0#) → eucQuot x y ≈ eucQuot' x y nz  
  lemma {x} {y} nz  with y ≟ 0#   
  ...                          | no _    =  ≈refl   
  ...                          | yes y=0 =  ⊥-elim (nz y=0)

where  divRem  has the last argument irrelevant.
This is type-checked in  
                        darcs MAlonzo of January 8, 2014.
  
Now I try to add irrelevance to  eucQuot'  and to  lemma
(without any sensible reason for this, just for testing) :

  -- (II)
  eucQuot' : (x y : C) → .(nz : y ≉ 0#) → C
  eucQuot' x y _ =  quot $ divRem x y _

  lemma : {x y : C} → .(nz : y ≉ 0#) → eucQuot x y ≈ eucQuot' x y _
  lemma {x} {y} _  with y ≟ 0#
  ...                          | no _    =  ≈refl
  ...                          | yes y=0 =  ⊥-elim (? y=0)

                                            -- where    
                                            -- nz' : y ≉ 0#
                                            -- nz' = _  

1) I cannot prove it without using  "with y ≟ 0# ".

2) the checker requires the  `yes'  branch too, 
   and  yes ()  is rejected, it needs  "= ⊥-elim ...".

3) Now, what to put for the above `?'  ? 
   nz  is irrelevant and cannot be used here,  
   underscore  causes "unsolved metas".

4) `where' in the end also causes "unsolved metas".
   This looks strange:  it knows what to put for `_' after {y} and does
   not know this for  "nz' = _".

So, I have  .(nz : y ≉ 0#)  and  y=o  and do not see how to map this to
⊥.

Thank you in advance for explanation.

------
Sergei