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

(U::into_iter).ensures((other,), zip_iter_snd(r)),

zip_iter_fst(r) == i,

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

IteratorSpec::produces(&r)
    == i
        .produces()
        .zip_truncate(zip_iter_snd(r).produces())
        .map_values(|p: (bool, bool)| p.0 && p.1),

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