title: what is the type of a here
body: <p>I found this code</p>
  
  <pre><code>Lemma foldlP T S f (s : seq T) x0 (I : nat -&gt; S -&gt; Prop) : 
  I 0%N x0 -&gt; 
  (forall i x a, (i &lt; size s)%N -&gt; I i x -&gt; I i.+1 (f x (nth a s i))) -&gt; 
  I (size s) (foldl f x0 s).
  </code></pre>
  
  <p><a href="http://poleiro.info/posts/2019-12-24-a-verification-challenge.html" rel="nofollow noreferrer">here</a> and am trying to understand how it works. I think I get the general idea, but I can't figure out what type the variable a is, or, indeed, what purpose it is serving as an argument to nth. I can't run the code on my own IDE as I have looked around for a Seq library in coq and have not found one. Based on my general understanding of sequences alone, I have no clue what information the a is carrying.</p>
  
  <p>Thank you!</p>