Nuprl - Pf auto2_lemma_6 1 1 1 1 1 2 1 1 1 1 1 1 1 2 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 2 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))

a1,a2:(n-1). f(a1) = f(a2) {t:T| t = f(n-1) } a1 = a2

By: UnivCD

Generated subgoals:

1 8. a1: (n-1)
9. a2: (n-1)
10. f(a1) = f(a2) {t:T| t = f(n-1) }
a1 = a2

2 8. a1: (n-1)
9. a2: (n-1)
f(a1) {t:T| t = f(n-1) }

3 8. a1: (n-1)
9. a2: (n-1)
f(a2) {t:T| t = f(n-1) }

About:

1	8. `a1:` `(n-1)` 9. `a2:` `(n-1)` 10. `f(a1) = f(a2) {t:T\| t = f(n-1) }` `a1 = a2`
2	8. `a1:` `(n-1)` 9. `a2:` `(n-1)` `f(a1) {t:T\| t = f(n-1) }`
3	8. `a1:` `(n-1)` 9. `a2:` `(n-1)` `f(a2) {t:T\| t = f(n-1) }`