Nuprl - Pf auto2_lemma

PrintForm Definitions exponent Sections AutomataTheory Doc

1. n:

T:Type, R:(TProp). (f:(nT). Bij(n; T; f)) & (t:T. Dec(R(t))) Dec(t:T. R(t))

By: NatInd 1

Generated subgoals:

1 T:Type, R:(TProp). (f:(0T). Bij(0; T; f)) & (t:T. Dec(R(t))) Dec(t:T. R(t))

2 1. n:
2. 0 < n
3. T:Type, R:(TProp). (f:((n-1)T). Bij((n-1); T; f)) & (t:T. Dec(R(t))) Dec(t:T. R(t))
T:Type, R:(TProp). (f:(nT). Bij(n; T; f)) & (t:T. Dec(R(t))) Dec(t:T. R(t))

About:

1	`T:Type, R:(TProp). (f:(0T). Bij(0; T; f)) & (t:T. Dec(R(t))) Dec(t:T. R(t))`
2	1. `n:` 2. `0 < n` 3. `T:Type, R:(TProp). (f:((n-1)T). Bij((n-1); T; f)) & (t:T. Dec(R(t))) Dec(t:T. R(t))` `T:Type, R:(TProp). (f:(nT). Bij(n; T; f)) & (t:T. Dec(R(t))) Dec(t:T. R(t))`