The point of these tests is that binders with wrong indices will be undebruijnified successfully, whereas variables with wrong indices (e.g. out of scope) will fail.