title: Using `apply with` without giving names of parameters in Coq?
body: <p>In using the Coq <code>apply ... with</code> tactic, the examples I have seen all involve explicitly giving the names of variables to instantiate. For example, given a theorem about the transitivity of equality.</p>
  
  <pre><code>Theorem trans_eq : forall (X:Type) (n m o : X),
    n = m -&gt; m = o -&gt; n = o.
  </code></pre>
  
  <p>To <code>apply</code> it:</p>
  
  <pre><code>Example test: forall n m: nat,
    n = 1 -&gt; 1 = m -&gt; n = m.
  Proof.
    intros n m. 
    apply trans_eq with (m := 1). Qed.
  </code></pre>
  
  <p>Note that in the last line <code>apply trans_eq with (m := 1).</code>, I have to remember that the name of the variable to instantiate is <code>m</code>, rather than <code>o</code> or <code>n</code> or some other names <code>y</code>. </p>
  
  <p>To me, whether <code>m n o</code> or <code>x y z</code> are used in the original statement of the theorem shouldn't matter, because they are like dummy variables or formal parameters of a function. And sometimes I can't remember the specific names I used or somebody else put down in a different file when defining the theorem. </p>
  
  <p>Is there a way by which I can refer to the variables e.g. by their position and use something like:</p>
  
  <pre><code>apply trans_eq with (@1 := 1)
  </code></pre>
  
  <p>in the above example?</p>
  
  <p>By the way, I tried: <code>apply trans_eq with (1 := 1).</code> and got <code>Error: No such binder.</code> </p>
  
  <p>Thanks.</p>