The Instantiation of the Induction Scheme
The induction scheme just shown is just an abbreviation for our
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.