PrintForm Definitions finite sets Sections AutomataTheory Doc

At: fin dec fin 2
1. n:
2. 0 < n
3. T:Type, B:(TProp). (f:((n-1)T), g:(T(n-1)). InvFuns((n-1); T; f; g)) & (t:T. Dec(B(t))) (m:, f:(m{t:T| B(t) }), g:({t:T| B(t) }m). InvFuns(m; {t:T| B(t) }; f; g))
4. T: Type
5. B: TProp
6. f: nT
7. g: Tn
8. InvFuns(n; T; f; g)
9. t:T. Dec(B(t))

m:, f:(m{t:T| B(t) }), g:({t:T| B(t) }m). InvFuns(m; {t:T| B(t) }; f; g)
By:
Unfold `inv_funs` 8
THEN
GenRepD
Generated subgoal:

18. g o f = Id
9. f o g = Id
10. t:T. Dec(B(t))
m:, f:(m{t:T| B(t) }), g:({t:T| B(t) }m). InvFuns(m; {t:T| B(t) }; f; g)

About:
existsfunctionnatural_numbersetapplyintless_than
alluniversepropimpliesandsubtract