Nuprl - Pf auto2_lemma_6 1 1 1 1 1 2 1 1 1 1 1 1

1. n:
2. 0 < n
3. T: Type
4. R: TProp
5. f: nT
6. Bij(n; T; f)
7. t:T. Dec(R(t))

(f@0:((n-1){t:T| t = f(n-1) }). Bij((n-1); {t:T| t = f(n-1) }; f@0)) & (t:{t:T| t = f(n-1) }. Dec(R(t)))

By: Analyze 0

Generated subgoals:

1 f@0:((n-1){t:T| t = f(n-1) }). Bij((n-1); {t:T| t = f(n-1) }; f@0)

2 t:{t:T| t = f(n-1) }. Dec(R(t))

About:

1	`f@0:((n-1){t:T\| t = f(n-1) }). Bij((n-1); {t:T\| t = f(n-1) }; f@0)`
2	`t:{t:T\| t = f(n-1) }. Dec(R(t))`