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

PrintForm Definitions exponent Sections AutomataTheory Doc

At: auto2 lemma 6 1 1 1 1 1 2 1 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)

By: Witness f

Generated subgoals:

1 f (n-1){t:T| t = f(n-1) }

2 Bij((n-1); {t:T| t = f(n-1) }; f)

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

About:

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