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

i.obeys_prophetic_iter_laws(),

i.decrease() is Some,

forall |k| 0 <= k < i.remaining().len() ==> call_requires(f, (&i.remaining()[k],)),

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

ensures

{
    let keep = filter_keep(r);
    {
        &&& keep.len() <= i.remaining().len()
        &&& forall |j| {
            0 <= j < keep.len()
                ==> call_ensures(f, (&i.remaining()[j],), #[trigger] keep[j])
        }
        &&& IteratorSpec::remaining(&r)
            == i.remaining()[..keep.len()].filter_index(|j: int| keep[j])
        &&& 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]
                        && call_ensures(f, (&i.remaining()[j],), true)
                }
        }
        &&& IteratorSpec::will_return_none(&r)
            ==> i.will_return_none() && keep.len() == i.remaining().len()
        &&& IteratorSpec::decrease(&r) is Some == i.decrease() is Some
        &&& filter_iter(r) == i
        &&& filter_fun(r) == f

    }
},