Also fix induction_pr_arg so that it adds the right attribute inside the goal.
This will create a new commit in order to revert the existing changes.
