Subgoal *1/2.
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.