Function lemma_filter_view_commute 

pub proof fn lemma_filter_view_commute<S: View>(
    s: Seq<S>,
    p: FnSpec<(S,), bool>,
    sp: FnSpec<(S::V,), bool>,
)

requires

forall |s: S| p(s) <==> sp(s.view()),

ensures

s.filter(p).map_values(|x: S| x.view()) == s.map_values(|x: S| x.view()).filter(sp),

Filtering a sequence and then viewing its elements produces the same result as viewing the elements first and then filtering with the corresponding predicate. The predicates p and sp must be equivalent under view.

Example

proof fn example() {
    let s = seq!["hello".to_string(), "world".to_string()];
    let p = |x: String| x.len() > 4;
    let sp = |x: Seq<char>| x.len() > 4;

    let way1 = s.filter(p).map_values(|x| x.view());
    let way2 = s.map_values(|x| x.view()).filter(sp);
    assert(way1 == way2);
}