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.
