Remove length indexing

This allows us to have more Haskell-like types and ‘List Text’ in
exchange for some uglier proofs.
Work directly on Vec
Get into Substrings