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

1. n:
2. 0 < n
3. T: Type
4. R: TProp
5. f: nT
6. Inj(n; T; f)
7. b:T. a:n. f(a) = b
8. t:T. Dec(R(t))
9. b: T
10. b = f(n-1)

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

By: Witness7 b

Generated subgoal:

1 7. t:T. Dec(R(t))
8. b: T
9. b = f(n-1)
10. a:n. f(a) = b
a:(n-1). f(a) = b {t:T| t = f(n-1) }

About: