PrintForm Definitions exponent Sections AutomataTheory Doc

At: auto2 lemma 6 1 1 1 1 1 2 1
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))
4. T: Type
5. R: TProp
6. (f:(nT). Bij(n; T; f)) & (t:T. Dec(R(t)))

Dec(t:T. R(t))
By: Analyze 6
Generated subgoal:

16. f:(nT). Bij(n; T; f)
7. t:T. Dec(R(t))
Dec(t:T. R(t))

About:
existsapplyintless_thannatural_numberall
universefunctionpropimpliesandsubtract