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.