Who Cites rel 1 1?
rel_1_1	Def  R is 1-1 == x,x':A, y,y':B. R(x,y) & R(x',y')  (x = x'  y = y')
	Thm*  A,B:Type, R:(ABProp). (R is 1-1)  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:

R is 1-1

has structure:

rel_1_1(A; B; R)

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