## Overview of the Expansion of ENDP in the Induction Step

In this message the system is saying that `Subgoal *1/2`

has been
rewritten to the `Subgoal *1/2'`

, by expanding the definition of **endp**.
This is an example of **simplification**, one of the main proof
techniques used by the theorem prover.

Click here if you would like to step through the
simplification of `Subgoal *1/2`

.