After using `x`, we know it is active.
Next we use and activate `y`, which has to pop `Uniq(x)` as they have distinct tags.
Finally, we use `x` again even though it is no longer in the stack, triggering UB.
-(A `Uniq` is only veer pushed when it is created, so it is never in the stack more than once.)
+(A `Uniq` is only ever pushed when it is created, so it is never in the stack more than once.)
### 4.2 Barriers