Alph*Alph*Prop

nAlph

Alphn

InvFuns(n; Alph; f; g)

x,y:Alph*. Dec(x E y)

h:(n*n*). (x,y:n*. (x (x,y. map(f;x) E map(f;y)) y) h(x) = h(y)) & (x:n*. x (x,y. map(f;x) E map(f;y)) (h(x)))

h:(Alph*Alph*). (x,y:Alph*. (x E y) h(x) = h(y)) & (x:Alph*. x E (h(x)))

1	9. h: n*n* 10. (x,y:n*. (x (x,y. map(f;x) E map(f;y)) y) h(x) = h(y)) & (x:n*. x (x,y. map(f;x) E map(f;y)) (h(x))) h:(Alph*Alph*). (x,y:Alph*. (x E y) h(x) = h(y) Alph*) & (x:Alph*. x E (h(x)))

About: