Nuprl - Proof: listify length 1 1 1 2

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

1. T : Type
2. m :

3. n :

4. f : {m..n

}

T
5. m

n
6.

m:{...n}, f:({m..n

}

T). ||f{m..n

}|| = n-m

||f{m..n

}|| = n-m

By:	BackThru -1

Generated subgoals:

None

About:

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