Function axiom_hash_set_with_view_spec_lenCopy item path

pub broadcast proof fn axiom_hash_set_with_view_spec_len<Key>(m: &HashSetWithView<Key>)
where
    Key: View + Eq + Hash,

#[trigger] m.spec_len() == m@.len(),