fsdoc: no-summary-found
fsdoc: no-comment-found
Abstractly, a `vec a l` is just a sequence whose length is `U32.v l`. `reveal` and `hide` build an isomorphism establishing this *