Function rev_postcondition 

pub broadcast proof fn rev_postcondition<I: DoubleEndedIteratorSpec>(i: I, r: Rev<I>)

requires

#[trigger] rev_post(i, r),

ensures

IteratorSpec::remaining(&r) == IteratorSpec::remaining(&i).reverse(),

IteratorSpec::produces(&r) == i.produces().reverse(),

IteratorSpec::decrease(&r) is Some == i.decrease() is Some,