Dex proves indexing correctness without a full dependent type system, including loops.

See: https://github.com/google-research/dex-lang/pull/969 and https://github.com/google-research/dex-lang/blob/5cbbdc50ce0... for examples