Nuprl - Pf auto2_lemma

PrintForm Definitions exponent Sections AutomataTheory Doc

1. T: Type
2. R: TProp
3. Fin(T)
4. t:T. Dec(R(t))

Dec(t:T. R(t))

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

Generated subgoals:

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

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

About:

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