By default, structural induction induct t produces an induction hypothesis for the variables directly mentioned in t, and rule induction induct rule: p.induct produces a hypothesis for the variables directly mentioned by the eliminated p assumption.

Sometimes you need a stronger hypothesis that generalises across additional variables in the goal. The arbitrary option tells the induct method to generalise certain variables, so the induction hypothesis assumes the property holds for all values of those variables.