Nuprl - Proof: select append back 1 2 1

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

1. T : Type
2. T List
3. bs : T List
4. T
5. v : T List
6.

i:{||v||..(||v||+||bs||)

}. (v @ bs)[i] = bs[(i-||v||)]
7. i : {(||v||+1)..(||v||+1+||bs||)

}

(v @ bs)[(i-1)] = bs[(i-(||v||+1))]

By:	Witness6 i-1

Generated subgoal:

1 6. i : {(||v||+1)..(||v||+1+||bs||)}
7. (v @ bs)[(i-1)] = bs[(i-1-||v||)]
(v @ bs)[(i-1)] = bs[(i-(||v||+1))]
1 step

About:

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