[Agda] Type error?? But I'm sure it's well-typed!

[David Leduc]

Nils Anders Danielsson <nad at cs.nott.ac.uk> wrote:
> What can we do about this? We can abstract over p:

Thank you very much! This is very helpful.
I can use similar trick in my development, but then I face a new problem:
Because I abstract the necessary expression (like p here, but more complicate),
it is replaced by a variable.
This is a loss of information that prevents me from finishing my proof.
I have tried to use inspect in order to keep the original expression,
but then your trick does not work and the with fails.
Would you have any advice on how to deal with that?