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

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

ensures

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

IteratorSpec::produces(&r).len() == IteratorSpec::remaining(&r).len(),

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

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

map_iter(r) == i,

map_fun(r) == f,