theorem :: ABCMIZ_A:56

for C being initialized ConstructorSignature
for t1, t2, t being expression of C st t is_a_unification_of t1,t2 holds
( t matches_with t1 & t matches_with t2 )