Lift internal pack function from cpack into "global" primpack.

I think it may have useful lemmas to be proven of it.
Slight polishing in HOL primitives.
Prove that the cleanup phase of cpack does work.

It relies on the RFOR phase to
1. keep the list of elements in dinv distinct
2. keep all elements in dinv < N
3. to keep visited up to date (an index in visited is true iff that
   value is in dinv)
4. to not have updated dinv past index N

These conditions (plus boring ones about vector sizes not changing)
are in the packScript file at lines 106--107.