The Coq mailing list

[Jonas Oberhauser <s9joober AT gmail.com>]

Am 08.11.2012 23:08, schrieb Alan Schmitt:
> 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

You choose fun x => ~ f x x.
Then you prove H:(f x x <-> ~ f x x).
Then you prove B:(f x x). (By H you have to prove ~ f x x. Intros G: f x
x. apply H. Use G twice).
The rest is trivial.