:: deftheorem defines is_a_unification_of ABCMIZ_A:def 27 :
for C being initialized ConstructorSignature
for t, t1, t2 being expression of C holds
( t is_a_unification_of t1,t2 iff ex f being valuation of C st
( f unifies t1,t2 & t = t1 at f ) );