Intuitionize gsumreidx (#4997)

* Add seqfveq2g to iset.mm

This is seqfveq2 from set.mm with set existence conditions added.
The proof is the set.mm proof with only small changes for set existence.

* Add seqfveqg to iset.mm

This is seqfveq from set.mm with set existence conditions added.  The
proof is the set.mm proof with small changes for set existence.

* Add seqsplitg to iset.mm

This is seqsplit from set.mm with set existence conditions added.  The
proof is the set.mm proof with small changes for set existence.

* Add seqshft2g to iset.mm

This is seqshft2 from set.mm with set existence conditions added.  The
proof is the set.mm proof with a few small changes for set existence.

* add change bound variable theorems to iset.mm

This is cbvaldvaw , cbvexdvaw , cbval2vw , and cbvex2vw .
Stated as in set.mm including the same distinct variables, but proofs
and axiom usage may be different.

* Add seqm1g to iset.mm

This is seqm1 from set.mm with set existence conditions added.  The
proof is from seq3m1 .

* Add seqf1og to iset.mm

This is similar to seq3f1o in iset.mm and seqf1o in set.mm but the
conditions are slightly different.  The proof, including lemmas,
is the set.mm proof with changes in various places for set existence,
decidability of various propositions, and differences in seq theorems.

Includes lemmas seqf1oglem2a , seqf1oglem1 , and seqf1oglem2 which
are based on seqf1olem2a , seqf1olem1 , and seqf1olem2 from set.mm.

* Add gsumfzreidx to iset.mm

The statement of the theorem is gsumreidx in set.mm with the addition of
conditions that M and N are integers.  The proof is a new one from
gsumfzval and seqf1og .

Author: jkingdon