The Justification of the Induction Scheme

This paragraph explains why the induction selected is legal. The explanation is basically the same as the explanation for why the recursion in (APP A B) terminates.