let C be 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 )
let a, b be 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 t1, t2 be expression of C, a_Type C; ( (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)
; ( 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; verum