:: deftheorem defines Goto SCMFSA8A:def 1 :
for l being Nat holds Goto l = Load (goto l);