title: Coq Record Types
body: <p>I am new to Coq. I get an error when I try to define two record types that have type fields with the same name. For example: </p>
  
  <pre><code>Record squag := {
      U : Type;
      op : U -&gt; U -&gt; U where "x * y" := (op x y);
      idempotent_op : forall x : U, (x * x) = (x);
      commutative_op : forall x y : U, (x * y) = (y * x);
      antiAbsorbent_op : forall x y: U, (x * (x * y)) = (y)
  }.
  Record dummy := { 
      U : Type; 
      zero : U
  }.
  </code></pre>
  
  <p>The error I get is: </p>
  
  <blockquote>
    <p>Error: U already exists.</p>
  </blockquote>
  
  <p>Any help is appreciated. </p>