reconsider
x
=
Head
s
as
Element
of
INT
;
the
Tran
of
T
.
[
(
s
`1_3
)
,
(
(
s
`3_3
)
.
x
)
]
is
Tran-Goal
of
T
;
hence
the
Tran
of
T
.
[
(
s
`1_3
)
,
(
(
s
`3_3
)
.
(
Head
s
)
)
]
is
Tran-Goal
of
T
;
:: thesis:
verum