Fix: proper renaming of bound substitutions

Added a fix for a bug discovered recently by usage of Tautology.

When a substitution is made inside a formula with a binder, the bound variable is not taken into account for further recursive generation of new identifiers. This is now fixed by tracking a set of extra taken IDs.

It was failing in the following example (minified):

Substitute with formula variable s, s -> (z = y) (trivial substitution that does nothing here, but has a free variable y):

Original:
∧(∀'y_1. ¬(∀'y. ¬('y = 'y_1)))
Expected:
∧(∀'y_1. ¬(∀'y. ¬('y = 'y_1)))
Output:
∧(∀'y_1. ¬(∀'y_1. ¬('y_1 = 'y_1)))

Added this test case as well.