for x1, x2 being variable
for C1, C2 being initialized ConstructorSignature st x1 -term C1 = x2 -term C2 holds
x1 = x2