[Agda] question on `with'

[Sergei Meshveliani]

Please, what is wrong in the following program?

-------------------------------------------------------------------------
open import Data.Bool        using (Bool; true; false; _≟_)
open import Data.Nat         using (ℕ)
open import Relation.Nullary using (yes; no)
open import Relation.Binary.PropositionalEquality using (_≡_)


f :  (P : ℕ → Bool) → ℕ → ℕ
f P x
    with  P x | P x ≟ false

... | _ | yes eq =  0
                    where debug : P x ≡ false
                          debug = eq
... | _ | _ =  1

-------------------------------------------------------------------------

Agda 2.5.1.1 reports that  eq  has not the declared type.


Thanks,

------
Sergei