title: Coq: Proof of list pair
body: <p>I have wrote this Inductive predicate and part of the proof for its (strong) specification:</p>
  <pre><code>Inductive SumPairs : (nat*nat) -&gt; list (nat*nat) -&gt; Prop :=
  | sp_base : SumPairs (0,0) nil
  | sp_step : forall (l0:list (nat*nat)) (n0 n1: nat) (y:(nat*nat)), SumPairs (n0,n1) l0 -&gt; 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.
  ...
  </code></pre>
  <p>The thing is I don't think the theorem is correct because Coq doesn’t accept something like <code>{n0 n1: nat | ...}</code>. Is there a way to fix that or am I thinking wrong?</p>
  <p>I think the predicate <code>SumPairs</code> is correct, but since I'm not sure, here's an example of how it should work: input <code>[(1,2),(3,4)]</code>, expected output <code>[3,7]</code></p>