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))

TProp

nT

Tn

t:T. Dec(B(t))

f (n-1){t:T| g(t) < n-1 }

g {t:T| g(t) < n-1 }(n-1)

m{t:{t:T| g(t) < n-1 }| B(t) }

{t:{t:T| g(t) < n-1 }| B(t) }m

(m+1){t:T| B(t) }

f2 = (x.if x=m f(n-1) else f1(x) fi)

{t:T| B(t) }(m+1)

g2 = (x.if g(x)=n-1 m else g@0(x) fi)

(m+1)

if g(if x=m f(n-1) else f1(x) fi)=n-1 m else g@0(if x=m f(n-1) else f1(x) fi) fi = x (m+1)

1	24. x = m 25. g(f(n-1)) = n-1 m = x (m+1)
2	24. x = m 25. g(f(n-1)) = n-1 g@0(f(n-1)) = x (m+1)
3	24. x = m 25. g(f1(x)) = n-1 m = x (m+1)
4	24. x = m 25. g(f1(x)) = n-1 g@0(f1(x)) = x (m+1)

About: