Nuprl - Proof: list iso 2 2 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: list iso 2 2 1

1. 'a : S
2. x : (

'a)

f:(

'a), n:

. x = <

. if m<

n then f(m) else @

x:'a. true

fi ,n>

x':'a List. x = rep_list('a;x')

By:	Last Analyze THEN Last Analyze THEN StrongAuto THEN Try (Complete (Unfold `label` 0))

Generated subgoal:

1 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')
15 steps

About:

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