pub broadcast proof fn lemma_ref_obeys_eq_spec<T: PartialEq>()
obeys_eq::<T>(),
#[trigger] obeys_eq::<&T>(),