The Coq mailing list

[Alexander Kogtenkov <kwaxer AT mail.ru>]

> Didn’t you mean "Axiom A: forall c c': C, (~ (c = c')) <-> (~ (F c = F> 
> c'))"?

Yes, that works as well.

Regards,
Alexander Kogtenkov


Sun, 20 Jul 2014 22:52:56 +0200 от Cédric 
<sedrikov AT gmail.com>:
> Le Sun, 20 Jul 2014 21:39:34 +0200, 
> <kwaxer AT mail.ru>
>  a écrit:
> 
> > Hi,
> >
> > Given the following environment
> >
> > Variable C: Set.
> > Variable N: Set.
> > Variable F: C-> N.
> > Axiom A: forall c c': C, (~ (c = c')) = (~ (F c = F c')).
> 
> Didn’t you mean "Axiom A: forall c c': C, (~ (c = c')) <-> (~ (F c = F  
> c'))"?
> Your original axiom seems dubious to me.
> 
> >
> > how one can prove
> >
> > Theorem T: forall (n: N) (c: С), F c = n -> forall c': C, F c' = n -> c  
> > = c'.
> >
> > ?
> >
> > I believe this requires the proof of
> >
> > Lemma L: forall A B: Prop, (~ A) = (~ B) -> A = B.
> >
> > How can it be done? Can this be avoided as I guess the lemma requires
> > classical logic?
> >
> > Thank you,
> > Alexander Kogtenkov
> 
> 
> -- 
> ---
> Cédric AUGER