The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 07/20/2014 03:39 PM, 
kwaxer AT mail.ru
 wrote:
> 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')).
>
> 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

I think this just requires decidable equality on C.

-- Jonathan