<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.
<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.