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 a given or goal in 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.