:: deftheorem defines idval ABCMIZ_1:def 59 :
for C being initialized ConstructorSignature
for X being Subset of Vars holds C idval X = { [x,(x -term C)] where x is variable : x in X } ;