Function zip_post 

pub uninterp spec fn zip_post<I, U, Z>(i: I, other: U, r: Z) -> bool