:: deftheorem defines goto SCMRING2:def 8 :
for R being Ring
for l being Nat holds goto (l,R) = [6,<*l*>,{}];