let C be initialized ConstructorSignature; :: thesis: 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 )
let a, b be expression of C, an_Adj C; :: thesis: 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 )
let t1, t2 be expression of C, a_Type C; :: thesis: ( (ast C) term (a,t1) = (ast C) term (b,t2) implies ( a = b & t1 = t2 ) )
assume (ast C) term (a,t1) = (ast C) term (b,t2) ; :: thesis: ( a = b & t1 = t2 )
then [*, the carrier of C] -tree <*a,t1*> = (ast C) term (b,t2) by Th46
.= [*, the carrier of C] -tree <*b,t2*> by Th46 ;
then <*a,t1*> = <*b,t2*> by TREES_4:15;
hence ( a = b & t1 = t2 ) by FINSEQ_1:77; :: thesis: verum