At: fin dec fin21111 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)) 11. x: (n-1)
g(f(x)) < n-1 By: RWH add_composeC 0
THEN
HypSubst 8 0
THEN
Reduce 0 Generated subgoals:
T:Type, B:(T
Prop).
(
f:(
(n-1)
(
g(f(x)) < n-1
