Nuprl - Proof: listify length 1 1 1 1 2 1

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

1. T : Type
2. n :

3. m : {...n-1}
4.

f:({(m+1)..n

}

T). ||f{(m+1)..n

}|| = n-(m+1)
5. f : {m..n

}

T
6. m<n

||f{(m+1)..n

}||+1 = n-m

By:	Witness4 f

Generated subgoals:

None

About:

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