feat: size lemma for Array.set!

[fgdorais]

No description provided.

Hmm, actually if Array.set!_is_setD is already a simp lemma then this seems somewhat unnecessary.

[fgdorais]

@eric-wieser I just realized there is an ambiguity in your last comment. I read it to mean that the simp was not necessary but you might have meant that the lemma wasn't necessary?

I do have use cases where this lemma is useful but simp is more awkward, often in '(...) arguments to getElem. For example, I would like to use (xs.set! ...)[i]'(xs.size_get! .. ▸ ...) rather than a by simp proof in some cases.