Def  (x:A. B(x)) ~ (x':A'. B'(x'))
Def  == f:(AA'), g:(A'A), F:(x:AB(x)B'(f(x))), G:(x:AB'(f(x))B(x)).
Def  == InvFuns(A;A';f;g) & (u:A. InvFuns(B(u);B'(f(u));F(u);G(u)))

is mentioned

In prior sections: DiscreteMath

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html