[Agda] Defining a module by pattern matching

[Guillaume Brunerie]

Hi,

I have several definitions all starting with the following arguments:
{x x' : A} {p : x == x'} {u : Π (B x) (C x)} {u' : Π (B x') (C x')}

In order to make the code more readable, I would like to wrap them in
a section so that I can write the arguments only once.
The issue is that all those definitions are defined by pattern
matching on p, so I cannot do it and I need to copy paste the list of
arguments for each definition which makes the code quite hard to read.

Is there a way to workaround this issue? Some way to define a
parametrized module by pattern matching, or something like that?

Thanks,

Guillaume