Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

x,y:. (x = y) x = y

Applied Tactic: Auto
Generated subgoals:

None