Function axiom_key_model_implies_obeys_eq 

pub broadcast proof fn axiom_key_model_implies_obeys_eq<Key: Hash + Eq + ?Sized>()

requires

#[trigger] obeys_key_model::<Key>(),

ensures

<Key as PartialEqSpec>::obeys_eq_spec(),

forall |a: &Key| #[trigger] a.eq_spec(a),

forall |a: &Key, b: &Key| #[trigger] a.eq_spec(b) <==> b.eq_spec(a),

forall |a: &Key, b: &Key, c: &Key| {
    a.eq_spec(b) && #[trigger] b.eq_spec(c) ==> #[trigger] a.eq_spec(c)
},

The key model supplies faithful equality and equivalence laws, including for unsized keys.