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),