pub broadcast proof fn axiom_spec_len<T>(slice: &[T])
#[trigger] spec_slice_len(slice) == slice@.len(),