Nuprl - Proof: listify wf 1

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

1. T : Type

, m,n:

. n-m

(

f:({m..n

}

T). f{m..n

}

T List)

By:	CompNatInd Concl THEN UnivCD

Generated subgoal:

1 2. k :
3. k1:. k1<k (m,n:. n-mk1 (f:({m..n}T). f{m..n} T List))
4. m :
5. n :
6. n-mk
7. f : {m..n}T
f{m..n} T List
5 steps

About:

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