i does_not_destroy intloc 0 by Def6;
then reconsider Mi = Macro i as good Program of SCM+FSA by SCMFSA8C:99;
Mi ';' J is good ;
hence i ';' J is good ; :: thesis: verum