pub broadcast proof fn axiom_set_ext_equal_deep<A>(s1: Set<A>, s2: Set<A>)Expand description
ensures
#[trigger] (s1 =~~= s2) <==> (s1 =~= s2),Sets s1 and s2 are considered equal if and only if they contain all of the same elements.
This has to be an axiom because Set is external_body.