Signed-off-by: Jim Pryor <profjim@jimpryor.net>
and there's no more mutation going on there than there is in:
- <!--
- <pre>
- <code>∀x. (F x or ∀x (not (F x)))</code>
- </pre>
- -->
+ <pre><code>∀x. (F x or ∀x (not (F x)))
+</code></pre>
When a previously-bound variable is rebound in the way we see here, that's called **shadowing**: the outer binding is shadowed during the scope of the inner binding.