Function vstd::std_specs::hash::axiom_contains_deref_key
source · pub broadcast proof fn axiom_contains_deref_key<Q, Value>(m: Map<Q, Value>, k: &Q)Expand description
ensures
#[trigger] contains_borrowed_key::<Q, Value, Q>(m, k) <==> m.contains_key(*k),