Function lemma_key_model_implies_obeys_eq 

pub broadcast proof fn lemma_key_model_implies_obeys_eq<Key: Hash + Eq>()

requires

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

ensures

crate::laws_eq::obeys_eq::<Key>(),