[Agda] question on `with'

[Roman]

You matched on `P x` with a wildcard pattern, Agda introduced a dummy
variable `w` for it and rewrote `P x`  to `w` everywhere in the
context, hence the type of `eq` is `w ≡ false`.

Here is how you can make it work:

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

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