title: Coq true = false discriminate fails, no primitive equality
body: <p>I'm trying to prove the following, and I think I have the right approach to solving by enumerating all the cases for <code>b</code> and all the single argument boolean functions <code>f</code> (should be 4 functions over 2 boolean values), proving the point by exhaustively destructing everything.</p>
  
  <pre><code>Theorem example :
    forall (f : bool -&gt; bool) (b : bool),
    f (f b) = b.
  Proof.
    intros.
    destruct (f (f b)).
    - destruct b. 
      + reflexivity. 
      + Fail discriminate. admit. 
    - destruct b eqn:Hqebb.
      + Fail discriminate. admit. 
      + reflexivity.  
  Qed.
  </code></pre>
  
  <p>However, when I try to discriminate on the 2nd and 3rd steps, on <code>false = true</code> I get the following error:</p>
  
  <pre><code>Ltac call to "discriminate" failed.
  No primitive equality found.
  </code></pre>
  
  <p>I've used discriminate before with inductive types and it worked as expected, so I was surprised it didn't work here with boolean types. Any ideas why?</p>