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