Function vstd::std_specs::hash::axiom_set_box_key_to_value

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