:: deftheorem defines Zeroseq RSSPACE:def 6 :
Zeroseq = seq_const 0;