[Agda] `let postulate ... in'

[Sergei Meshveliani]

Please, what may be a work around for  ``let postulate ...'' in  

  case P? y of \
  { (yes _) →  let postulate fx=fy : f x =' f y
               in  here fx=fy
  ; ...
  }
  where
  ...
?

Agda-2.3.2.1 does not type-check  `let postulate'.
It does accept  ...
                where
                postulate ...,

but `where' is not allowed in this place of  ` -> ...'  of `case'.

(Most often I set `postulate' as temporary, for debugging. Debugging
becomes easier, and further I replace `postulate' with implementation). 

Thanks,

------
Sergei