Previously Used Names
Invariant under weak binding of belongs to.