a := b does_not_destroy intloc 0 by SCMFSA7B:12;
hence a := b is good by Def6; :: thesis: verum