{t:T| g(t) < n-1 } 
Type 
(n-1) Type {t:T| g(t) < n-1 } Type f (n-1)
{t:T| g(t) < n-1 } g {t:T| g(t) < n-1 }(n-1)
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))PropnTnt:T. Dec(B(t)) (n-1){t:T| g(t) < n-1 } {t:T| g(t) < n-1 }(n-1) f o g = f o g| 1 | {t:T| g(t) < n-1 } Type |
| 2 | (n-1) Type |
| 3 | {t:T| g(t) < n-1 } Type |
| 4 | f (n-1){t:T| g(t) < n-1 } |
| 5 | g {t:T| g(t) < n-1 }(n-1) |
About:
 |  |  |  |  |  |  |  |
 |  |  |  |  |  |  |