## 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`

.