Who Cites rel implies?
rel_implies	Def R1 => R2 == x,y:T. (x R1 y)  (x R2 y)
	Thm* T:Type, R1,R2:(TTProp). R1 => R2  Prop

Syntax:

R1 => R2

has structure:

rel_implies(T; R1; R2)

About: IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html