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