In this message the system is saying that Subgoal *1/2' has been
rewritten to T using the rules noted. The word ``But'' at the beginning
of the sentence is a signal that the goal has been proved.
Click here to step through the proof of Subgoal *1/2'.
