While the user is wondering how to proceed in the proof, the tutors are
trying to progress in the proof. After a while, the tutors' suggestions
start to appear in the lower part of the \hbugs{} interface window
-(the topmost window in Fig. \ref{prima}). In this case, the tutors are able
+(the topmost window in Fig. \ref{step1}). In this case, the tutors are able
to produce 23 hints. The first and not very useful hint suggests to proceed in
the proof by exchanging the two sides of the equality.
The second hint suggests to reduce both sides of the equality to their normal