Def A ~~ B == f:(AB), g:(BA). InvFuns(A; B; f; g)

is mentioned by

Thm* (f:(AB). Bij(A; B; f))  (A ~~ B)

[bij_iff_1_1_corr]

Try larger context: StandardLIB IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html