Function vstd::std_specs::hash::axiom_set_box_key_removed

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