Level: Lib Thy Top: 1
Hypotheses:

  1. St :

  2. Fin(St)

Conclusion:

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

Applied Tactic: D 2
Generated subgoals:

1. eq:St St . x,y:St. (eq x y) x = y