for C being initialized ConstructorSignature
for a being positive expression of C, an_Adj C holds Non a = (non_op C) term a