No more internal eq rewrite contractive

This primitive rule has always appeared very ad-hoc to me. And indeed, as shown in this merge request, we do not need it for proving the lemmas in boxes, so I propose to get rid of it.