Level:
Lib
Thy
Top
:
1
1
Hypotheses:
n :
Conclusion:
n@0:
.
f:
n@0
n. Bij(
n@0;
n;f)
Applied Tactic:
With
n
(D 0) THENW Auto
Generated subgoals:
1
.
f:
n
n. Bij(
n;
n;f)
n@0:. f:n@0 
n. Bij(n@0;n;f)
n
(D 0) THENW Autof:n n. Bij(n;n;f)