Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Using sigT and existT

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Using sigT and existT


chronological Thread 
  • From: Adam Chlipala <adamc AT csail.mit.edu>
  • To: Ramon <i AT ramon.org.il>
  • Cc: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Using sigT and existT
  • Date: Thu, 29 Dec 2011 09:10:38 -0500

Ramon wrote:
I am playing around with Coq, and got stuck when trying to prove:

Lemma existT_equal
     : forall T F (X : T) a b,
         existT F X a = existT F X b ->
             a = b.

This fact is independent of CIC. That is, it is neither provable nor disprovable. The standard library establishes [existsT_equal] under the name [EqDep.inj_pair2], appealing to an axiom. When [T] has decidable equality, you can give an axiom-free proof, for instance with [Eqdep_dec.inj_pair2_eq_dec].



Archive powered by MhonArc 2.6.16.

Top of Page