## Stream: general

### Topic: implicit conv congr

#### Patrick Massot (Oct 06 2018 at 16:43):

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

#### Patrick Massot (Oct 07 2018 at 21:25):

@Mario Carneiro did you see this question?

#### Mario Carneiro (Oct 08 2018 at 00:32):

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

#### Patrick Massot (Oct 08 2018 at 09:04):

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

Last updated: May 09 2021 at 19:11 UTC