Def  AB == {fg:((AB)(BA))| fg/f,g. InvFuns(A;B;f;g) }

is mentioned by

Thm*  (a bij a) ~ (aa)	[nsub_bij_ooc_invpair]
Thm*  ((AB)) ~ (A ~ B)	[inv_pair_inv2]
Thm*  (AB) ~ (A ~ B)	[inv_pair_inv]
Thm*  (A ~ A')  (B ~ B')  ((AB) ~ (A'B'))	[inv_pair_functionality_wrt_one_one_corr]
Thm*  ((AB))  (A ~ B)	[inv_pair_iff_ooc]
Def  fin_enum(A) == k:kA	[fin_enum]

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