Def (i, j)(x) == if x=i j ; x=j i else x fi

is mentioned by

Thm* k:, x,y,i:k. (y, x)((y, x)(i)) = i	[flip_twice]
Thm* k:, x,y:k. (y, x) o (y, x) = (x.x)	[flip_inverse]
Thm* k:, i,j:k. Bij(k; k; (i, j))	[flip_bijection]
Thm* k:, i,j:k. (i, j) = (j, i)	[flip_symmetry]
Thm* n:, f:(n), i:(n-1). sum(f((i, i+1)(x)) | x < n) = sum(f(x) | x < n)	[sum_switch]

Try larger context: MarkB generic IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html