:: deftheorem defines is_a_general-unification_of ABCMIZ_A:def 28 :
for C being initialized ConstructorSignature
for t, t1, t2 being expression of C holds
( t is_a_general-unification_of t1,t2 iff ( t is_a_unification_of t1,t2 & ( for u being expression of C st u is_a_unification_of t1,t2 holds
u matches_with t ) ) );