SubFrom a,b does_not_destroy intloc 0 by SCMFSA7B:14;
hence SubFrom a,b is good by Def6; :: thesis: verum