let
l1
,
l2
be
Nat
;
:: thesis:
(
goto
l1
=
goto
l2
implies
l1
=
l2
)
assume
A1
:
goto
l1
=
goto
l2
;
:: thesis:
l1
=
l2
(
<*
l1
*>
.
1
=
l1
&
<*
l2
*>
.
1
=
l2
)
by
FINSEQ_1:40
;
hence
l1
=
l2
by
A1
,
XTUPLE_0:3
;
:: thesis:
verum