theorem Th8: :: SCMFSA10:8

for a being Int-Location
for il being Nat holds a >0_goto il = [8,<*il*>,<*a*>]