theorem :: ABCMIZ_1:47

for C being initialized ConstructorSignature
for a, b being expression of C, an_Adj C
for t1, t2 being expression of C, a_Type C st (ast C) term (a,t1) = (ast C) term (b,t2) holds
( a = b & t1 = t2 )