Def  (f {to n}  f' {to n'})(i) == if in f(i) else f'(i) fi

is mentioned by

Thm*  n:, f:({1...n}Peg), n':. Thm*  nn' Thm*   Thm*  (f':({n+1...n'}Peg), i:{1...n'}. Thm*  (n<i  (f {to n}  f' {to n'})(i) = f'(i))	[hanoi_extend_higheq]
Thm*  n:, f:({1...n}Peg), n':. Thm*  nn' Thm*   Thm*  (f':({n+1...n'}Peg), i:{1...n'}. Thm*  (in  (f {to n}  f' {to n'})(i) = f(i))	[hanoi_extend_loweq]
Def  (s(?) {to n}  h {to n'})(x) == s(x) {to n}  h {to n'}	[hanoi_seq_deepen]

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