Infer Menu:

Reflexive Law Command

The reflexive law for equality says that for any object x, x=x. To use this law, select the gap in which you want to apply the reflexive law (or the goal of the gap) and give the Reflexive Law command. A dialog box will open asking what object you want to use for x in the reflexive law. Enter an expression naming some object and click OK, and Proof Designer will assert that the object is equal to itself.

If your goal has the form x=x, for some object x, then you can select the goal and give the Reflexive Law command, and Proof Designer will infer the goal without opening a dialog box.