* 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.
