Level: Lib Thy Top: 1 1
Hypotheses:

  1. T :

  2. S :

  3. f : T S

  4. Fin(S)

  5. s:S. Dec(t:T. f t = s)

Conclusion:

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

Applied Tactic: Assert EquivRel(T;x,y.f x = f y)
Generated subgoals:

1. EquivRel(T;x,y.f x = f y)

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