vstd::seq_lib

Function lemma_fold_left_permutation

Source 
pub proof fn lemma_fold_left_permutation<A, B>(
    l1: Seq<A>,
    l2: Seq<A>,
    f: FnSpec<(B, A), B>,
    v: B,
)
Expand description
requires
commutative_foldl(f),
l1.to_multiset() == l2.to_multiset(),
ensures
l1.fold_left(v, f) == l2.fold_left(v, f),