Function axiom_spec_iter Copy item path

pub broadcast proof fn axiom_spec_iter<'a>(s: &'a str)

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