Description: Principle of Finite Induction (inference schema), using implicit
substitutions. The first three hypotheses establish the substitutions
we need. The last two are the basis and the induction step. Theorem
Schema 22 of Suppes p. 136. (Contributed by NM, 22-Mar-2006)