Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

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

Applied Tactic: (RepD ...a)
Generated subgoals:

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