Fix bug in bound variables check; add regression tests

[ulrikrasmussen]

The current check only works reliably when all variables are either bound or unifies with a constant, but it sometimes fails to realize that a variable is unified via binary unifiers to a bound variable.

Sometimes a possibly unbound variable ends up being the representative for the set of variables that it unifies with, in which case subst.get() just returns the possibly unbound variable.

The solution is to 1) expand the set of known bound variables to include all variables in the image of the derived substitution, and 2) apply the substitution to a possibly unbound variable and check if the result is bound if the other checks fail.

There may be a more clever way of doing this which I haven't realized.

[aaronbembenek]

Thanks for identifying this bug and fixing it -- much appreciated! :)