Autoinduct performs induction on the right argument of a recursive function. The tactic was originally used in a course by T. Ringer. Find a link to the implementation here.