PrintForm Definitions exponent Sections AutomataTheory Doc

At: auto2 lemma 6 1 1 1 1 1 2 1 1 1 1
1. n:
2. 0 < n
3. 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))
By: Witness8 R
Generated subgoal:

18. (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:
existsapplyintless_thannatural_numberuniversefunction
propallsetequalsubtractimpliesand