Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Question about proof with single negation and equality

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Question about proof with single negation and equality


Chronological Thread 
  • From: <kwaxer AT mail.ru>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] Question about proof with single negation and equality
  • Date: Sun, 20 Jul 2014 21:39:34 +0200

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



Archive powered by MHonArc 2.6.18.

Top of Page