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.