[Agda] problem using "with"

[Guillermo Calderón]

hello,

I have a problem using  "with".  The  code below  is a simplified 
version to illustrate the case:


 > g :  ℕ  → ℕ
 > g a with  a ≤? 5
 > ... |  yes _  = a
 > ... |  no  _  = suc a
 >
 > prop-g  : ∀ n  -> (R :  ℕ  → Set)
 >                -> (∀ m -> R (suc m))
 >                -> (∀ n -> n ≤ 5 -> R (g n))
 >                -> R (g n)
 > prop-g n R f1 f2  with n ≤? 5
 > ... | no  ¬p   =  f1 n
 > ... | yes p    =  f2 n p- -*** ERROR here ***
 >

_≤?_  is the decidable total order relation from the standard library 
Data.Nat

Agda gives this error message:

 > g n | n ≤? 5 != n of type ℕ
 > when checking that the expression f2 n p has type R (g n | yes p)

However  (g n)  reduces to n   for the case  | yes p.

What's wrong with the above?

Thanks for your help.

Guillermo