title: taking the first type in the list of tuple
body: <p>I had a list <code>l</code> has type: <code>l: list (list (A * B * C * D))</code> and I would like it returns for me a type <code>list (list A)</code></p>
  
  <p>I am trying the code with <code>split</code> function with the argument <code>list (A * B * C * D)</code>to see the result. </p>
  
  <pre><code>Require Import List.
  Variables A B C D : Type.
  Definition split_list (l: list (A * B * C * D)) : list (A * B * C) * list D 
             := split l.
  </code></pre>
  
  <p>How can I write the function?</p>