is mentioned by

Thm* f:(AB), g:(BA). InvFuns(A; B; f; g)  Bij(A; B; f)	[fun_with_inv_is_bij]
Thm* f:(AB). Bij(A; B; f)  (g:(BA). InvFuns(A; B; f; g))	[bij_imp_exists_inv]
Thm* f:(AB), g:(BA). SqStable(InvFuns(A; B; f; g))	[sq_stable__inv_funs]
Def A ~~ B == f:(AB), g:(BA). InvFuns(A; B; f; g)	[one_one_corr]

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