Reverse loops?

[Timmmm]

If I try to verify a reversed loop like

for i in (0..len).rev()

I get this error

error[E0277]: the trait bound `std::iter::Rev<std::ops::Range<usize>>: vstd::pervasive::ForLoopGhostIteratorNew` is not satisfied
  --> src/main.rs:43:5
   |
43 | /     for i in (0..len).rev()
44 | |         invariant
45 | |             len == v.len(),
46 | |             del <= i,
...  |
53 | |         }
54 | |     }
   | |_____^ the trait `vstd::pervasive::ForLoopGhostIteratorNew` is not implemented for `std::iter::Rev<std::ops::Range<usize>>`
   |
   = help: the following other types implement trait `vstd::pervasive::ForLoopGhostIteratorNew`:
             std::collections::hash_map::Keys<'a, Key, Value>
             std::collections::hash_set::Iter<'a, Key>
             std::collections::vec_deque::Iter<'a, T>
             std::ops::Range<A>

error[E0277]: the trait bound `std::iter::Rev<std::ops::Range<usize>>: vstd::pervasive::ForLoopGhostIteratorNew` is not satisfied
  --> src/main.rs:43:14
   |
43 |     for i in (0..len).rev()
   |              ^^^^^^^^^^^^^^ the trait `vstd::pervasive::ForLoopGhostIteratorNew` is not implemented for `std::iter::Rev<std::ops::Range<usize>>`
   |
   = help: the following other types implement trait `vstd::pervasive::ForLoopGhostIteratorNew`:
             std::collections::hash_map::Keys<'a, Key, Value>
             std::collections::hash_set::Iter<'a, Key>
             std::collections::vec_deque::Iter<'a, T>
             std::ops::Range<A>

error: aborting due to 2 previous errors

Is that expected? Is there a solution to this? I guess the obvious thing is

for i in 0..len {
  let i = len - i - 1;

but that's not very satisfying.