:: deftheorem defines SCM-goto AMI_3:def 8 :
for loc being Nat holds SCM-goto loc = [6,<*loc*>,{}];