Who Cites flip?
flip	Def (i, j)(x) == if x=i j ; x=j i else x fi
	Thm* k:, i,j:k. (i, j)  kk
eq_int	Def i=j == if i=j true ; false fi
	Thm* i,j:. (i=j)

Syntax:

(i, j)

has structure:

flip(i; j)

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