Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
T,S:
. Fin(T)
1-1-Corresp(T;S)
Fin(S)
Applied Tactic:
Unfold `finite` 0 THEN Unfold `one_one_corr` 0 THEN UnivCD THENW Auto
Generated subgoals:
1
.
n:
.
f:
n
S. Bij(
n;S;f)
T,S:
. Fin(T) 
1-1-Corresp(T;S) 
Fin(S)
n:
. f:n 
S. Bij(n;S;f)