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