Description: Principle of Finite Induction (inference schema), using implicit
substitutions. The first four hypotheses establish the substitutions we
need. The last two are the basis and the induction step. Theorem
Schema 22 of Suppes p. 136. This is Metamath 100 proof #74.
(Contributed by NM, 14-Apr-1995)