* Simple tactic for substitution of equals for equals and equivalent for equivalents.
* Some corrections in the EquivalenceChecker
* Moved InstantiateBinder to helpers.
* Some more changes regarding tactics and proof steps.