Nuprl - Pf fun_enumer 1 2 1 2

1. n:
2. m:
3. 0 < m
4. f: ((m-1)n)(nm-1)
5. Bij((m-1)n; (nm-1); f)
6. n = 0

f:((mn)(nm)). Bij(mn; (nm); f)

By: Inst Thm* n,m:. f:(nm(nm)). Bij(nm; (nm); f) [n;(nm-1)]

Generated subgoals:

1 0 < (nm-1)

2 7. f:(n(nm-1)(n(nm-1))). Bij(n(nm-1); (n(nm-1)); f)
f:((mn)(nm)). Bij(mn; (nm); f)

About:

1	`0 < (nm-1)`
2	7. `f:(n(nm-1)(n(nm-1))). Bij(n(nm-1); (n(nm-1)); f)` `f:((mn)(nm)). Bij(mn; (nm); f)`