Example with refinements

[ecranceMERCE]

Currently, the type of vectors related to a function dropping the nat parameter and returning list. The problem is that this encoding makes it impossible to define a partial inverse function going back to vectors without having an inhabitant of the parameter to cover the case where the list is smaller than the expected index n.

Defining a version of vectors and lists taking an inhabited type {A : Type & A} as a parameter would be cumbersome because we would have to redefine all the operations on these custom versions, which brings back the complexity of handling Σ-types we wanted to avoid by relating vectors to lists in the first place (otherwise we would have chosen the following association:

Vector.t A n ~ {l : list A & length l = n}

The problem looks similar in the case of relating matrices to arrays of arrays, as this last container type does not have an index constraining its length.

[CohenCyril]

@ecranceMERCE a _CoqProject entry is missing to make the CI assess the new content.
I will add it.