Function vstd::std_specs::hash::axiom_set_deref_key_to_value

source · 
pub broadcast proof fn axiom_set_deref_key_to_value<Q>(m: Set<Q>, k: &Q, v: &Q)
Expand description
ensures
#[trigger] sets_borrowed_key_to_key::<Q, Q>(m, k, v) <==> m.contains(*k) && k == v,