Function vstd::std_specs::hash::axiom_deref_key_removed

source · 
pub broadcast proof fn axiom_deref_key_removed<Q, Value>(
    old_m: Map<Q, Value>,
    new_m: Map<Q, Value>,
    k: &Q
)
Expand description
ensures
#[trigger] borrowed_key_removed::<Q, Value, Q>(old_m, new_m, k)
    <==> new_m == old_m.remove(*k),