let x1, x2 be variable; :: thesis: for C1, C2 being initialized ConstructorSignature st x1 -term C1 = x2 -term C2 holds
x1 = x2
let C1, C2 be initialized ConstructorSignature; :: thesis: ( x1 -term C1 = x2 -term C2 implies x1 = x2 )
assume x1 -term C1 = x2 -term C2 ; :: thesis: x1 = x2
then [x1,a_Term] = [x2,a_Term] by TREES_4:4;
hence x1 = x2 by XTUPLE_0:1; :: thesis: verum