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