Function map_postcondition 

pub broadcast proof fn map_postcondition<I, F>(i: I, f: F, r: Map<I, F>)
where
    I: IteratorSpec,
    F: FnMut<(I::Item,)>,

requires

i.obeys_prophetic_iter_laws(),

#[trigger] map_post(i, f, r),

ensures

IteratorSpec::remaining(&r).len() <= i.remaining().len(),

forall |k| {
    0 <= k < IteratorSpec::remaining(&r).len()
        ==> call_ensures(f, (i.remaining()[k],), IteratorSpec::remaining(&r)[k])
},

IteratorSpec::will_return_none(&r)
    ==> i.will_return_none() && IteratorSpec::remaining(&r).len() == i.remaining().len(),

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

map_iter(r) == i,

map_fun(r) == f,