Function vstd::set::axiom_set_ext_equal_deep

source · 
pub broadcast proof fn axiom_set_ext_equal_deep<A>(s1: Set<A>, s2: Set<A>)
Expand description
ensures
#[trigger] (s1 =~~= s2) <==> s1 =~= s2,