Function axiom_spec_slice_iter

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