Function vstd::std_specs::hash::axiom_box_key_removed

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