:: deftheorem defines are_weakly-unifiable ABCMIZ_A:def 26 :
for C being initialized ConstructorSignature
for t1, t2 being expression of C holds
( t1,t2 are_weakly-unifiable iff ex g being one-to-one irrelevant valuation of C st
( variables_in t2 c= dom g & t1,t2 at g are_unifiable ) );