reflexivity
Prev Chapter 7. Tactics Next

reflexivity

reflexivity

Synopsis:

reflexivity

Pre-conditions:

The conclusion of the current sequent must be t=t for some term t

Action:

It closes the current sequent by reflexivity of equality.

New sequents to prove:

None.

Prev Up Next
normalize Home replace