title: Using "symmetry" within Coq expressions
body: <p>I'm trying to figure out how to do the following in Coq. Say we have proved the following:</p>
  
  <p>trans_lemma: a = b -> b = c -> a = c</p>
  
  <p>and we want to use it to deduce that</p>
  
  <p>b = a -> c = b -> a = c.</p>
  
  <p>I can't seem to be able to get "apply trans_lemma with ..." to work whatever I do. It would seem like I would need to rewrite equations in trans_lemma, so that the variables would match in the same order. Is there some trivial way of doing this without reproving the lemma, i.e. can I somehow apply the "symmetry" tactic on an equation within an expression?</p>
  
  <p>(I know I can prove what I want without using the lemma by just using a few intros and rewrites, but I would like to know if there's a syntactic way of reusing the result that I already have.)</p>