Nuprl - Proof: listify select id 1 2

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

1. T : Type
2. as : T List
3.

n,j:

. j+||as|| = n

(

i.as[(i-j)]){j..n

} = as

(

||as||. as[i]){

||as||} = as

By:	(InstHyp [\|\|as\|\|;0] 3) THEN (ArithSimp -1)

Generated subgoals:

None

About:

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