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

1. n:
2. 0 < n
3. T: Type
4. R: TProp
5. f: nT
6. a1,a2:n. f(a1) = f(a2) a1 = a2
7. Surj(n; T; f)
8. t:T. Dec(R(t))
9. x: (n-1)
10. f(x) = f(n-1)

False

By: Witness6 x

Generated subgoal:

1 6. Surj(n; T; f)
7. t:T. Dec(R(t))
8. x: (n-1)
9. f(x) = f(n-1)
10. a2:n. f(x) = f(a2) x = a2 n
False

About: