:: deftheorem defines term ABCMIZ_1:def 29 :
for C being initialized ConstructorSignature
for c being constructor OperSymbol of C st len (the_arity_of c) = 0 holds
c term = [c, the carrier of C] -tree {};