a :=len f does_not_destroy intloc 0 by SCMFSA7B:22;
hence a :=len f is good by Def6; :: thesis: verum