:: deftheorem defines CZeroseq CSSPACE:def 6 :
CZeroseq = NAT --> 0c;