for C being initialized ConstructorSignature
for a being expression of C, an_Adj C holds vars ((non_op C) term a) = vars a by Th94;