2 | 3. T:Type{i}, B:(T Prop{i}).
( 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{i} 5. B: T Prop{i} 6. f: n T 7. g: T  n 8. g o f = Id 9. f o g = Id 10. t:T. Dec(B(t)) 11. f (n-1) {t:T| g(t) < n-1 } 12. g {t:T| g(t) < n-1 }  (n-1) (n-1) = (n-1) |