take
T
=
TBAStruct
(#
{
0
}
,
op1
,
op3
#);
:: thesis:
(
T
is
trivial
& not
T
is
empty
)
thus
(
T
is
trivial
& not
T
is
empty
) ;
:: thesis:
verum