Level: Lib Thy Top: 1
Hypotheses:

  1. T :

  2. U :

  3. 1-1-Corresp(T;U) Fin(T)

Conclusion:

Fin(U)

Applied Tactic: D 3
Generated subgoals:

1. Fin(U)