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