Don't freshen uniques on universally quantified variables when instantiating equalities.
Make induction hypothesis applications loud (temporary).