Function vstd::set::fold::lemma_fold_empty

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,

Function vstd::set::fold::lemma_fold_emptyCopy item path