[Agda] irrelevant arg example

[Sergei Meshveliani]

Dear Agda developers,

Agda of August 19 2014  type-checks irrelevant arguments in a different
way than  Agda-2.4.0.2.
So that some of my code is not type-checked any more.
I have the two questions on the subject.

1. Which treating is more correct?

2. For example, how to implement the function

  f : (x : ℕ) → .(nz : x ≢ 0) → x ≢ 0   
  f x ???

?

Thanks,

------
Sergei