coq - Coq: リストペアの証明

Question

私はこの帰納的述語とその (強い) 仕様の証明の一部を書きました:

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.
...

問題は、Coq が のようなものを受け入れないため、定理が正しいとは思わないことです{n0 n1: nat | ...}。それを修正する方法はありますか、それとも私の考えが間違っていますか?

述語は正しいと思いますSumPairsが、よくわからないので、どのように機能するかの例を次に示します: 入力[(1,2),(3,4)]、期待される出力[3,7]