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