title: example for introduction pattern (p1 & ... & pn) does not work
body: <p>I am reading the Coq (8.5p1) reference manual,</p>
  
  <blockquote>
    <p>introduction via (p1 &amp; ... &amp; pn) is a shortcut for introduction via
    (p1,(...,(...,pn)...)); it expects the hypothesis to be a sequence of
    right-associative binary inductive constructors such as conj or
    ex_intro; for instance, an hypothesis with type A/(exists x, B/\C/\D)
    can be introduced via pattern (a &amp; x &amp; b &amp; c &amp; d);</p>
  </blockquote>
  
  <p>Trying to test this out, I did:</p>
  
  <pre><code>Goal forall A B C D: Prop, A/\(exists x:nat, B/\C/\D) -&gt; D.
  intros (a &amp; x &amp; b &amp; c &amp; d).
  </code></pre>
  
  <p>But Coq is telling me:</p>
  
  <blockquote>
    <p>Error: Not an inductive product.</p>
  </blockquote>
  
  <p>And I got the same error for a few other variants, such as one without the <code>-&gt; D</code>.</p>
  
  <p>Can some one please explain what's the correct usage (in a hopefully useful example)?</p>