azul on Nostr: you need a function to rebuild with a higher bound. resize :: (m:Nat) -> BVec x n -> ...

you need a function to rebuild with a higher bound.

resize :: (m:Nat) -> BVec x n -> BVec x (n+m)
resize m [] = []
resize m (x :: xs) = x :: resize m xs

assuming that + is left-recursive