Function vstd::std_specs::hash::axiom_set_contains_box
source · pub broadcast proof fn axiom_set_contains_box<Q>(m: Set<Box<Q>>, k: &Q)Expand description
ensures
#[trigger] set_contains_borrowed_key::<Box<Q>, Q>(m, k) <==> m.contains(Box::new(*k)),