The Instantiation of the Induction Scheme

The induction scheme just shown is just an abbreviation for our real goal.

To obtain our actual goals we have to replace the schema :P by the associativity conjecture (instantiated as shown in the scheme).

This produces two actual goals, the induction step and the base case.