Def A =ext B == (X:A. X  B) & (X:B. X  A)

is mentioned by

Thm* A:Type. Sexpr(A) =ext (Sexpr(A)Sexpr(A))+A	[sfa_doc_sexpr_fp]
Thm* Void =ext (x:. {x:})	[sfa_doc_void_via_isect2]
Thm* Void =ext (A:Type. A)	[sfa_doc_void_via_isect]
Thm* VoidA =ext {x.x:VoidA}	[sfa_doc_void_dom_fun_degenerate]
Thm* Void List =ext {nil:Void List}	[sfa_doc_void_list_is_singleton]
Thm* VoidA =ext Void	[sfa_doc_void_cross_is_void]
Thm* Void =ext rec(A.A)	[sfa_doc_void_rectype]
Thm* P:(AProp), B:(x:AType(given P(x))). Thm* x:{u:A| P(u) }B(x) =ext x:AB(x)(given P(x))	[sfa_doc_exteq_gfun2]
Thm* B:(AProp), C:({u:A| B(u) }Type). Thm* x:{u:A| B(u) }C(x) =ext x:AC(x)(given B(x))	[sfa_doc_exteq_gfun]
Thm* P:(AProp). {x:A| P(x) }Prop =ext x:AProp(given P(x))	[sfa_doc_exteq_gprop]

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