Function axiom_spec_into_iter

Source
pub broadcast proof fn axiom_spec_into_iter<T, A: Allocator>(v: Vec<T, A>)
Expand description
ensures
(#[trigger] spec_into_iter(v))@ == (0int, v@),