2380 

  2380 

  2381   \noindent

  2381   \noindent

  2382   holds. This allows us to use the implication from the strong cases

  2382   holds. This allows us to use the implication from the strong cases

  2383   lemma, and we are done.

  2383   lemma, and we are done.

  2384 

  2384 

  2386   cases. This completes the proof establishing that the weak induction principles imply 

  2386   cases. This completes the proof establishing that the weak induction principles imply 

  2387   the strong induction principles. These strong induction principles have proved 

  2387   the strong induction principles. These strong induction principles have proved 

  2388   already to be very useful in practice, particularly for proving properties about 

  2388   already to be very useful in practice, particularly for proving properties about 

  2389   capture-avoiding substitution. 

  2389   capture-avoiding substitution. 

  2390 *}

  2390 *}