Correct invariants in example IntList-FH-JML.