Level: Lib Thy Top: 1
Hypotheses:

  1. T :

  2. S :

  3. f : T S

  4. Fin(S) (s:S. Dec(t:T. f t = s))

Conclusion:

Fin(x,y:T//(f x = f y))

Applied Tactic: D 4
Generated subgoals:

1. Fin(x,y:T//(f x = f y))