 # Using exists in pair proof

Hi! I have wrote this Inductive predicate and part of the proof for its specification:

``````Inductive SumPairs : (nat*nat) -> list (nat*nat) -> Prop :=
| sp_base : SumPairs (0,0) nil
| sp_step : forall (l0:list (nat*nat)) (n0 n1: nat) (y:(nat*nat)), SumPairs (n0,n1) l0 -> SumPairs ((n0+(fst y)),(n1+(snd y))) (cons y l0).

Theorem sumPairs_correct : forall (l:list (nat*nat)), { n: nat | SumPairs (n,n) l }.
Proof.
...
``````

The thing is I can’t complete it because I think I need a step like `exists ((x+(fst a))` for the first part of the pair and `exists ((x+(snd a))` for the second part but I don’t know how to express that in Coq. Is there a way to do that or am I thinking wrong?
Thank you!

That theorem is wrong: take `l = [(1, 2)]`, for example.

You’re right… Then is it possible to change that Theorem? The thing is Coq doesn’t accept something like `{n0 n1: nat | ...}`

I think you want `{ p: nat * nat | … (fst p) … (snd p) }`.

For short questions like this one you might prefer Coq’s Zulip channel, btw (You’ll get replies faster).

1 Like

`{'(n0,n1) | SumPairs (n0,n1) l }` works as well