The Coq mailing list

[Alan Schmitt <alan.schmitt AT polytechnique.org>]

Jonas Oberhauser 
<s9joober AT gmail.com>
 writes:

> One thing that has opened my eyes a little bit was this provable
> proposition that Smolka and CE Brown showed to me:
>
> Goal forall X, forall f : X -> (X -> Prop),  exists g, forall x, f x <> g.

I'd really like to see how you prove this. Just for fun, I tried it, and
I'm stuck at the very beginning:

  X : Type
  f : X -> X -> Prop
  ============================
   exists g : X -> Prop, forall x : X, f x <> g

What's the next step?

Alan