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