Function vstd::set::axiom_set_new

source · 
pub broadcast proof fn axiom_set_new<A>(f: FnSpec<(A,), bool>, a: A)
Expand description
ensures
#[trigger] Set::new(f).contains(a) == f(a),

A call to Set::new with the predicate f contains a if and only if f(a) is true.