In this message the system is saying that
Subgoal *1/2 has been rewritten
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