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