n:, m,a,z:, s1:({a...m}{1...n}Peg), s2:({m+1...z}{1...n}Peg).
  (s1 @(m) s2)  {a...z}{1...n}Peg

By:	Def of <fun> @(<int>) <fun> :{<int>...<int>}{1...<nat>}Peg THEN UnivCD

1

1. n :  2. m :  3. a :  4. z :  5. s1 : {a...m}{1...n}Peg 6. s2 : {m+1...z}{1...n}Peg   (x.if xm s1(x) else s2(x) fi)  {a...z}{1...n}Peg

2 steps

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