CHECK-STRUCTURE : MEXPRCHECK-STRUCTURE is a top-level command.
Check various structural properties of the current proof.
You will be informed about suspect constellations in the incomplete proof
which may make it difficult for ETPS to provide advice or for you to
finish the proof.
The command format for CHECK-STRUCTURE is:
TPS documentation homepage