:: deftheorem defines goto SCMPDS_2:def 4 :
for k1 being Integer holds goto k1 = [14,{},<*k1*>];