Def  AB == i:2. if i=0 A else B fi

is mentioned by

Thm*  (A bij B) ~ ((A inj B)(A onto B))	[bijtype_ooc_inj_isect_surjtype]
Thm*  (A bij B) =ext ((A inj B)(A onto B))	[bijtype_exteq_inj_isect_surjtype]

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