implicit conv congr

Stream: general

[Patrick Massot]

In conv mode, is there a version of congr/skip which allow traverse implicit arguments?

[Patrick Massot]

@Mario Carneiro did you see this question?

[Mario Carneiro]

I don't think congr decides things based on whether they are implicit, but rather whether they are dependent on other arguments

[Patrick Massot]

I made a few tests, and it seems you're right. So my new question is: how to you conv or rw dependent arguments? I guess this is the same issue I have when I want to use assumptions stating that two uniform structures are the same