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