Nuprl - Pf auto2_lemma_6 1 1 1 1 1 2 1 1 1 1 1 2 2 1 2 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 2 2 1 2 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:T| t = f(n-1) }. R(t))
8. R(f(n-1))
9. t: T
10. R(t)

False

By: Analyze 6

Generated subgoal:

1 6. Inj(n; T; f)
7. Surj(n; T; f)
8. (t:{t:T| t = f(n-1) }. R(t))
9. R(f(n-1))
10. t: T
11. R(t)
False

About: