title: coq change premise 'negation of not equal' to 'equal'
body: <p>Suppose I have a premise like this:</p>
  
  <pre><code>H2: ~ a b c &lt;&gt; a b c
  </code></pre>
  
  <p>And I wish to change it to:</p>
  
  <pre><code>a b c = a b c
  </code></pre>
  
  <p>Where</p>
  
  <p>a is Term -> Term -> Term</p>
  
  <p>b  and c are both Term</p>
  
  <p>How can I do it? Thanks!</p>