# another TCC question

```I have a theory in which I introduce a few types, and one operation; here
are the relevant types:

VERTEX_PAIR : TYPE+ = {x: finite_set[nat]| 0 < card(x) and card(x) < 3}

EDGE : TYPE = [# pair: VERTEX_PAIR, wt: nat #]

GRAPH : TYPE = finite_set[EDGE]

I then define the following operation:

g, g_result: VAR GRAPH
v1, v2, w: VAR nat

GotByIncluding(v1, v2, w, g, g_result): bool =
(g_result = union(g, singleton((# pair := {v: nat| v=v1 or v=v2},
wt := old_w
#))
))

When I typecheck the theory, this definition generates an unprovable TCC,
namely:

Insert_TCC1: OBLIGATION
(FORALL (x: [# pair: [nat -> bool], wt: nat #]): TRUE) AND
(FORALL (x: [nat -> bool]):
is_finite[nat](x) AND 0 < card[nat](x) AND card[nat](x) < 3);

Why is the second universal in this conjunctive TCC getting generated? I'm
being asked to show that any predicate on the naturals is finite and
between 0 and 3 in size???  There's probably some obvious point I'm
missing, but I'm not seeing it.

Anyone to the rescue?

Mark Aronszajn
WVU-RSRG

```