Hi! Is there a way to use `noconf`

to simplify an equality goal? Since `NoConfusionPackage`

contains both direction, it seems we could do the symmetric of what `noconf`

currently does right?

Yes, I think it's actually easily programmable, by looking up the NoConfusionPackage and applying the right lemma

But not in Ltac right? `repeat eapply noConfusion`

doesn't seem to be the best one can do.

I suppose you have `C x x' = C y y'`

in your goal and want to simplify to `(x, x') = (y, y')`

and then maybe two subgoals `x = y`

and `x' = y'`

? You will need to also try to apply the lemma about equality in sigma-types inbetween `apply noConfusion`

calls.

Yeah I expect to have a goal which is an equality between two elements of an inductive type (which I know) and would like to simplify it to equality between the different bits.

I was wondering if there was a general approach, I'll try something specialised I guess. Thanks.

Last updated: Jun 10 2023 at 23:01 UTC