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>
6. ||f{n}|| = n-0
7. m : 
8. m<n
9. m<||f{n}||
  (@x:'a. true) = arb('a)

By:	Inst Thm* 'a:S. equal(arb,select(x:'a. t)) [] THEN HN THEN StrongAuto THEN Try (Complete (Unfold `label` 0))

1

10. 'a:S. arb('a) = (@x:'a. true)   (@x:'a. true) = arb('a)

1 step

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