Refactor Data.Vec to use a refinement type ala `Fin`

[TOTBWF]

It might be worth considering replacing Data.Vec with a refinement type like

record Vec {ℓ} (A : Type ℓ) (n : Nat) : Type ℓ where
  constructor vec
  field
    lower : List A
    bounded : Irr (length lower ≡ n)

We still wont get good transports along refl due to transpList, but at least we can share functions between lists and vectors, and avoid storing the length of the vector on every cons-cell.

[plt-amy]

and avoid storing the length of the vector on every cons-cell.

agda already does this

[TOTBWF]

Ah, forgot about forcing analysis :) Still think that it could be worthwhile for code re-use reasons