Rodin Handbook


4.3.2 Identifier Xyz should not occur free in a witness

This means that the Xyz identifier appears in a witness predicate, but Xyz is a disappearing abstract variable or parameter and is not set as the witness label. To resolve this error, set change the witness label to the identifier Xyz.