title: Coq forward reasoning: apply with multiple hypotheses
body: <p>I have two hypothesis, and I would like to use forward reasoning to apply a theorem that uses both of them. </p>
  
  <p>My specific I have the hypothes</p>
  
  <pre><code>H0 : a + b = c + d
  H1 : e + f = g + h
  </code></pre>
  
  <p>and I want to apply the theorem from the standard library:</p>
  
  <pre><code>f_equal2_mult
       : forall x1 y1 x2 y2 : nat, x1 = y1 -&gt; x2 = y2 -&gt; x1 * x2 = y1 * y2
  </code></pre>
  
  <p>Now I know I could manually give the values for x1, y1, x2, y2, but I would like Coq to automatically determine those values when it unified with <code>H0</code> and <code>H1</code>.  I have figured out that I can get it to work like so:</p>
  
  <pre><code>eapply f_equal2_mult in H0; try exact H1.
  </code></pre>
  
  <p>But this feels like a hack, with the broken symmetry and the <code>try</code>.  I really would like to be able to say <code>apply f_equals2_mult in H0, H1</code> or something similarly clear.  Is there a way like this?</p>