PrintForm Definitions exponent Sections AutomataTheory Doc

At: auto2 lemma 6 1 1 2
1. T: Type
2. R: TProp
3. Fin(T)
4. t:T. Dec(R(t))
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))
By: Analyze 3
Generated subgoal:

13. n:
4. f:(nT). Bij(n; T; f)
5. t:T. Dec(R(t))
6. 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:
existsapplyuniversefunctionprop
allimpliesandnatural_number