Nuprl - Proof: listify wf 1 1 2 2

(8steps total) PrintForm Definitions list 1 Sections StandardLIB Doc

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

1. T : Type
2. k :

3.

k1:

. k1<k

(

m,n:

. n-m

k1

(

f:({m..n

}

T). f{m..n

}

T List))
4. m :

5. n :

6. n-m

k
7. f : {m..n

}

T
8. m<n

f{(m+1)..n

}

T List

By:	BackThru: Hyp:3 Using:[n-(m+1)]

Generated subgoals:

None

About:

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

(8steps total) PrintForm Definitions list 1 Sections StandardLIB Doc