1. 'a : S
2. x : ('a)
3. f : 'a
4. n : 
5. x = <m:. if m<n then f(m) else @x:'a. true fi ,n>
  x':'a List. x = rep_list('a;x')

By:	Subst (x = <m:. if m<n then f(m) else @x:'a. true fi ,n>) 0

1

x':'a List.    <m:. if m<n then f(m) else @x:'a. true fi ,n> = rep_list('a;x')

14 steps

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