pub broadcast proof fn ptrs_mut_eq_sized<T>(a: *mut T)
view_reverse_for_eq_sized::<T>((#[trigger] a@).addr, a@.provenance) == a,