Function vstd::set::fold::lemma_fold_insert

source · 
pub broadcast proof fn lemma_fold_insert<A, B>(s: Set<A>, z: B, f: FnSpec<(B, A), B>, a: A)
Expand description
requires
s.finite(),
!s.contains(a),
is_fun_commutative(f),
ensures
#[trigger] s.insert(a).fold(z, f) == f(s.fold(z, f), a),