Nuprl - Pf auto2_lemma_6 1 1 2 1 1 1 1

1. T: Type
2. R: TProp
3. n:
4. f:(nT). Bij(n; T; f)
5. t:T. Dec(R(t))
6. (f:(nT). Bij(n; T; f)) & (t:T. Dec(R(t))) Dec(t:T. R(t))

Dec(t:T. R(t))

By: Analyze 6

Generated subgoals:

1 (f:(nT). Bij(n; T; f)) & (t:T. Dec(R(t)))

2 6. Dec(t:T. R(t))
Dec(t:T. R(t))

About:

1	`(f:(nT). Bij(n; T; f)) & (t:T. Dec(R(t)))`
2	6. `Dec(t:T. R(t))` `Dec(t:T. R(t))`