Function rev_postcondition Copy item path

i.obeys_prophetic_iter_laws(),

i.initial_value_relation(&i),

rev_post(i, into_rev_spec(i)),

{
    let r = #[trigger] into_rev_spec(i);
    &&& IteratorSpec::remaining(&r) == IteratorSpec::remaining(&i).reverse()
    &&& IteratorSpec::will_return_none(&r) == i.will_return_none()
    &&& IteratorSpec::decrease(&r) is Some == i.decrease() is Some
    &&& IteratorSpec::initial_value_relation(&r, &r)

},