title: Coq eapply generates a goal with a question mark while proving existence of a function
body: <p>I would like to prove that for every group there exists a minus function that takes an element of the group and returns its negative.</p>
  
  <p>My Coq code is as follows:</p>
  
  <pre><code>Record Group:Type := {
  G:Set;
  plus: G-&gt;G-&gt;G;
  O:G;
  assoc: forall x y z:G, plus x (plus y z)=plus (plus x y) z;
  neut: forall x:G, plus x O=x /\ plus O x=x;
  neg: forall x:G, exists y:G, plus x y=O
  }.
  
  Lemma minus_exists(H:Group):exists minus_func:G H-&gt;G H, (forall x:G H, plus H x (minus_func(x))=O H).
  eapply ex_intro.
  </code></pre>
  
  <p>The last tactic generates the following output:</p>
  
  <pre><code>  H : Group
    ============================
     forall x : G H, plus H x (?12 x) = O H
  </code></pre>
  
  <p>My first issue is the <code>?12</code> which I figure is probably a badly displayed character. What is the meaning of this and is there a way to make it readable.</p>
  
  <p>My second question is how to complete the proof, which might become clearer after the first question is answered.</p>