Function zip_postcondition 

pub broadcast proof fn zip_postcondition<I, U>(
    i: I,
    other: U,
    r: Zip<I, <U as IntoIterator>::IntoIter>,
)
where
    I: Sized + IteratorSpec,
    U: IntoIterator,

requires

i.obeys_prophetic_iter_laws(),

#[trigger] zip_post(i, other, r),

ensures

call_ensures(U::into_iter, (other,), zip_iter_snd(r)),

zip_iter_fst(r) == i,

IteratorSpec::remaining(&r) == i.remaining().zip_truncate(zip_iter_snd(r).remaining()),

IteratorSpec::will_return_none(&r)
    ==> i.will_return_none() || zip_iter_snd(r).will_return_none(),

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