Function axiom_set_decreases_to_member 

pub broadcast proof fn axiom_set_decreases_to_member<A>(s: Set<A>, a: A)

requires

#[trigger] s.contains(a),

ensures

#[trigger] (decreases_to!(s => a)),

A member of a Set is less than that Set.