The basic idea of the plugin is to derive functions and proofs over indexed types like vectors from non-indexed versions of those types like lists. It can do this automatically for a certain class of types (when the index is determined by a fold over the new index, like the length of a list) without any extra user input. For example, you don’t have to supply the relation between lists and vectors; the tool finds it automatically.
This is a preliminary release of the tool, which has some glitches to iron out, but if you’re interested, take a look at the plugin and play with some of the examples. I’d love feedback, bug reports, external contributions, and so on.