This lemma encapsulates the useful pattern of getting access to a single element in the big-op, and at the same time changing the big-op statement but in a way that is trivial to adjust for all the other elements.
We should probably have this as well for the other big-ops, but I think I will need some help for the "2" versions... this one was already kind of nasty to figure out.^^