theorem Th1: :: RELOC:1

for k, loc being Nat holds IncAddr ((SCM-goto loc),k) = SCM-goto (loc + k)