Function vstd::seq_lib::lemma_fold_right_permutation

source · 
pub proof fn lemma_fold_right_permutation<A, B>(
    l1: Seq<A>,
    l2: Seq<A>,
    f: FnSpec<(A, B), B>,
    v: B
)
Expand description
requires
commutative_foldr(f),
l1.to_multiset() == l2.to_multiset(),
ensures
l1.fold_right(f, v) == l2.fold_right(f, v),