theorem :: ABCMIZ_A:54

for C being initialized ConstructorSignature
for t1, t2 being expression of C st t1,t2 are_unifiable holds
t1,t2 are_weakly-unifiable