Def  ij == j<i

is mentioned by

Def  (s1 @(m) s2)(x) == if xm s1(x) else s2(x) fi	[hanoi_seq_join]
Def  (f {to n}  f' {to n'})(i) == if in f(i) else f'(i) fi	[hanoi_extend]

In prior sections: bool 1 int 2

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