refactor: small iterator improvements (#11175)

This PR removes duplicated instance parameters in the standard library
and flips lemmas of the form `toList_eq_toListIter` into a form that is
suitable for `simp`.

Author: datokrat