Need new lexically-scoped domain introduction primitive

So that substitution rules can, you know, use loops. 🙂

N.b. all of these also involve #1043. 🤔

cc @a-alveyblanc @shawnl00

Here's how this could look:
```
dot(a, b, n):=domain({[i]: 0<=i

Start by reading issue #1043 alongside this issue and study the proposed domain(...) example, especially the fresh local symbol i. Done means agreeing on and implementing a lexically scoped domain-introduction primitive that lets substitution rules express loops.

Written by the indexing model from the issue text.