Function vstd::std_specs::hash::axiom_set_deref_key_removed

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