At: fin dec fin21 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. g o f = Id 9. f o g = Id 10. t:T. Dec(B(t))