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.