Nuprl - Proof: listify length 1 1 1 1 2

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

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

}

||f{m..n

}|| = n-m

By:	RecCaseSplit `listify`

Generated subgoal:

1 6. m<n
||f{(m+1)..n}||+1 = n-m
1 step

About:

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