Who Cites rel 1 1 b?
rel_1_1_b	Def  1-1 xA,yB. R(x;y) Def  == x,x':A, y,y':B. R(x;y) & R(x';y')  (x = x'  y = y')
	Thm*  A,B:Type, R:(ABType). (1-1 xA,yB. R(x;y))  Type
iff	Def  P  Q == (P  Q) & (P  Q)
	Thm*  A,B:Prop. (A  B)  Prop
rev_implies	Def  P  Q == Q  P
	Thm*  A,B:Prop. (A  B)  Prop

Syntax:

1-1 xA,yB. R(x;y)

has structure:

rel_1_1_b(A; B; x,y.R(x;y))

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