vstd::set::fold

Function lemma_fold_empty

Source
pub broadcast proof fn lemma_fold_empty<A, B>(z: B, f: FnSpec<(B, A), B>)
Expand description
ensures
#[trigger] Set::empty().fold(z, f) == z,