GraphRefine + CRefine: handle slightly more cases.

New testfile for graph-refine export with new handling code. Also
some slight tweaks to some CRefine proofs that will be needed to
remove DONT_TRANSLATE markers from certain key places in the seL4
code. These proofs are also compatible with previous seL4.