# Re: question on dependent typing

```Kurt,

This is essentially the same problem as before.
In c, the domain has been extended by the addition of d,
which is as you gave.  However, the value given to c in the
WITH expression should reflect its value before, so I
started by changing it to:

c := {x:(add(d, t`b)) | t`c(x)}
]

Minor note: since you're declaring c to be a set, I used set
notation instead of a lambda.  It's just syntactic sugar, but

This leads to the unprovable TCC

The problem is that if x=d, then we can't prove that x is in
b.  So we need to exclude d:

x /= d AND t`c(x)}
]

Now the first TCC is provable (using grind), but the second isn't:

FORALL (d, t):
FORALL (x1: int):
t`b(x1) AND t`c(x1) IFF add[int](d, t`b)(x1) AND x1 /= d AND t`c(x1);

If you run grind on this, you end up with the sequent

{-1}  integer_pred(d!1)
{-2}  t!1`b(d!1)
{-3}  t!1`c(d!1)
{-4}  (x1!1 = d!1)
|-------

In a sequent like this, you need to find a contradiction in
the hypotheses.  If you stare at it for awhile, you realize
that there is no contradiction.  If d was already in b, then
it should not be excluded from the value for c (in this case
add(d, t`b) = t`b).  So the final result is