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

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))
8. Dec(t:{t:T| t = f(n-1) }. R(t))

Dec(t:T. R(t))

By: Analyze 8

Generated subgoals:

1 8. t:{t:T| t = f(n-1) }. R(t)
Dec(t:T. R(t))

2 8. (t:{t:T| t = f(n-1) }. R(t))
Dec(t:T. R(t))

About:

1	8. `t:{t:T\| t = f(n-1) }. R(t)` `Dec(t:T. R(t))`
2	8. `(t:{t:T\| t = f(n-1) }. R(t))` `Dec(t:T. R(t))`