Function filter_postcondition 

pub broadcast proof fn filter_postcondition<I, F>(i: I, f: F, r: Filter<I, F>)
where
    I: IteratorSpec,
    F: FnMut(&I::Item) -> bool,

requires

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

ensures

{
    let keep = filter_keep(r);
    {
        &&& keep.len() == i.remaining().len()
        &&& forall |j| {
            0 <= j < keep.len() && !(#[trigger] keep[j])
                ==> i.produces()[j] && f.ensures((&i.remaining()[j],), false)
        }
        &&& forall |j| {
            0 <= j < keep.len() && #[trigger] keep[j]
                ==> {
                    let k = i.remaining()[..j].filter_index(|idx: int| keep[idx]).len()
                        as int;
                    IteratorSpec::produces(&r)[k]
                        ==> i.produces()[j] && f.ensures((&i.remaining()[j],), true)
                }
        }
        &&& IteratorSpec::remaining(&r) == i.remaining().filter_index(|j: int| keep[j])
        &&& IteratorSpec::produces(&r).len() == IteratorSpec::remaining(&r).len()
        &&& IteratorSpec::remaining(&r).len() <= i.remaining().len()
        &&& forall |k| {
            0 <= k < IteratorSpec::remaining(&r).len()
                ==> exists |j| {
                    0 <= j < i.remaining().len()
                        && IteratorSpec::remaining(&r)[k] == #[trigger] i.remaining()[j]
                        && keep[j]
                        && k
                            == i
                                .remaining()[..j]
                                .filter_index(|idx: int| keep[idx])
                                .len()
                        && (IteratorSpec::produces(&r)[k]
                            ==> i.produces()[j] && f.ensures((&i.remaining()[j],), true))
                }
        }
        &&& IteratorSpec::decrease(&r) is Some == i.decrease() is Some
        &&& filter_iter(r) == i
        &&& filter_fun(r) == f

    }
},