for C being initialized ConstructorSignature
for t1, t2, t being expression of C st t is_a_unification_of t1,t2 holds
t is_a_unification_of t2,t1