Capture avoiding substitution of witnesses in expressions.
If a binder would capture a variable then it is anonymized to deBruijn form.
Substitute a witness into some thing. In the target, if we find a named binder that would capture a free variable in the type to substitute, then we rewrite that binder to anonymous form, avoiding the capture.
substituteWithW that determines the set of free names in the
type being substituted, and starts with an empty binder stack.