pub broadcast proof fn axiom_spec_slice_iter<'a, T>(s: &'a [T])
(#[trigger] spec_slice_iter(s))@ == (0int, s@),