Function axiom_from_iterator_ensures Copy item path

pub broadcast proof fn axiom_from_iterator_ensures<A, I: Iterator<Item = A> + IteratorSpec>(
    iter: I,
)

#[trigger] into_iter_remaining::<A, I>(iter) == iter.remaining(),