pub broadcast proof fn axiom_string_hash_set_spec_len(m: &StringHashSet)Expand description
ensures
#[trigger] m.spec_len() == m@.len(),pub broadcast proof fn axiom_string_hash_set_spec_len(m: &StringHashSet)#[trigger] m.spec_len() == m@.len(),