Remove unneeded definition.
Style tweaks in compartmentalization proof.
Generalize definition of retag_set.