Move "simple loop" stuff into separate theory; prove stronger map result.

A map loop is one that is allowed to look at the old value of the
array at the index being updated. This subsumes the older result
because one could use the new lemma with an f instantiated so as to
ignore the old value.