IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
select append back1211 1. T : Type
2. T List
3. bs : T List
4. T 5. v : T List
6. i : {(||v||+1)..(||v||+1+||bs||)}
7. (v @ bs)[(i-1)] = bs[(i-1-||v||)]
(v @ bs)[(i-1)] = bs[(i-(||v||+1))]
By:
HypSubst 7 0
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
}
(v @ bs)[(i-1)] = bs[(i-(||v||+1))]
