theorem :: SCMFSA7B:12

for a, b being Int-Location
for l being Nat holds not b =0_goto l destroys a ;