Function axiom_spec_slice_iter Copy item path

pub broadcast proof fn axiom_spec_slice_iter<'a, T>(s: &'a [T])

#[trigger] spec_slice_iter(s).remaining() == s@.as_ref(),