:: deftheorem defines goto SCMFSA_2:def 13 :
for la being Nat holds goto la = SCM-goto la;