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.
(APP A B)
