coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: t x <txrev319 AT gmail.com>
- To: coq-club <coq-club AT inria.fr>
- Subject: [Coq-Club] Notions of Sets
- Date: Thu, 5 Sep 2013 20:20:26 +0000
[We're using propositional equivalence through all this.]
Here is a simple lemma. (I don't need help proving it. I need help making it more abstract).
(1)
Lemma lem__Z_split: forall (l r: Z) (P: Z -> Prop), (exists i, l <= i < r /\ P i) = (P l \/ (exists i, l +1 <= i < r)).
(2)
- [Coq-Club] Notions of Sets, t x, 09/05/2013
- Re: [Coq-Club] Notions of Sets, Arnaud Spiwack, 09/06/2013
- Re: [Coq-Club] Notions of Sets, Cedric Auger, 09/06/2013
- Re: [Coq-Club] Notions of Sets, t x, 09/06/2013
- Re: [Coq-Club] Notions of Sets, Cedric Auger, 09/06/2013
- Re: [Coq-Club] Notions of Sets, Arnaud Spiwack, 09/06/2013
Archive powered by MHonArc 2.6.18.