pub broadcast proof fn axiom_is_empty<A>(s: Set<A>)
!(#[trigger] s.is_empty()),
exists |a: A| s.contains(a),