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