Safer vcg in CRefine

[Xaphiosis]

As seen in this rambly gist
https://gist.github.com/Xaphiosis/2fa2b51b65e05c3addda1576f90a31ed

One way of getting around schematic unification disaster with the vcg method is via subset_refl. @lsf37 suggested we do this:

method svcg = rule conseqPre, vcg, rule order.refl

The question is whether we should look at anything else about this, deployment and the inevitable name bikeshed.