Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
T:
.
t:T. Fin(T)
Fin(T
T)
Applied Tactic:
(Unfold `finite` 0 THEN ExRepD ...a)
Generated subgoals:
1
.
n:
.
f:
n
(T
T). Bij(
n;T
T;f)
T:
. t:T. Fin(T) 
Fin(T 
T)
n:
. f:n 
(T T). Bij(n;T T;f)