Advanced vector properties

[suhr]

I want to prove leftpad with flux, and the corresponding property involves indexing into a vector and ensuring that the value at the index has a correct value. Is it possible to express this kind of property in Flux?

The proof of leftpad in Creusot uses quantifiers and the proof of leftpad in LiquidHaskell seems to rely on List being an algebraic type. But there seems to be no quantifiers in Flux and RVec is not an algebraic type.