PrintForm Definitions exponent Sections AutomataTheory Doc

At: auto2 lemma 6 1 1 1 1 1 2 1 1 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
7. Bij(n; T; f)
8. t:T. Dec(R(t))

Dec(t:T. R(t))
By: Witness3 {t:T| t = f(n-1) }
Generated subgoal:

13. T: Type
4. R: TProp
5. f: nT
6. Bij(n; T; f)
7. t:T. Dec(R(t))
8. R:({t:T| t = f(n-1) }Prop). (f@0:((n-1){t:T| t = f(n-1) }). Bij((n-1); {t:T| t = f(n-1) }; f@0)) & (t:{t:T| t = f(n-1) }. Dec(R(t))) Dec(t:{t:T| t = f(n-1) }. R(t))
Dec(t:T. R(t))

About:
existsapplysetequalsubtractnatural_numberint
less_thanalluniversefunctionpropimpliesand