I have such error message: `The term "imap fEmbedding l" has type "ilist domain' (relation_arities L R)" while it is expected to have type "ilist domain' (relation_arities L' (fRelations H R))"`

I have proof that `relation_arities L R = relation_arities L' (fRelations H R)`

. How can I use it to get rid of the error message?

Temporary (?) thing I did was to define function "aux" that transforms "ilist domain' (relation_arities L R)" to "ilist domain' (relation_arities L' (fRelations H R))" and use "imap fEmbedding (aux l)" instead of "imap fEmbedding l".

I looked what's inside the "aux" function and learned, hopefully, how to use eq_rect.

That's the right way to do it, and it does make reasoning harder, it's a known big drawback of dependent types.

The parameters to `eq_rect`

can be difficult to remember; there's a notation `rew H in x`

(in analogy to rewriting) from the standard library which makes `eq_rect`

easier to write and read. See https://github.com/tchajed/coq-tricks/blob/master/src/RewNotation.v for a working example.

Last updated: May 24 2024 at 22:02 UTC