Get rid of the definition `AttributeID_Node_Variant`
This definition is a quite complex function given as an enumerated set in definitions.def
.
This entails that each time we use it, we have to prove again and again that it is a function.
It would be better to abstract it away as a proper variable. I do not know exactly which degree of detail is needed to carry the other proofs that may depend on the precise value of this constant.
Edited by Laurent Voisin