1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
19 (*#***********************************************************************)
21 (* v * The Coq Proof Assistant / The Coq Development Team *)
23 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
25 (* \VV/ **************************************************************)
27 (* // * This file is distributed under the terms of the *)
29 (* * GNU Lesser General Public License Version 2.1 *)
31 (*#***********************************************************************)
33 (*#***************************************************************************)
37 (* Naive Set Theory in Coq *)
43 (* Rocquencourt Sophia-Antipolis *)
61 (* Acknowledgments: This work was started in July 1993 by F. Prost. Thanks *)
63 (* to the Newton Institute for providing an exceptional work environment *)
65 (* in Summer 1995. Several developments by E. Ledinot were an inspiration. *)
67 (*#***************************************************************************)
69 (*i $Id: Constructive_sets.v,v 1.5.2.1 2004/07/16 19:31:17 herbelin Exp $ i*)
71 include "Sets/Ensembles.ma".
74 Section Ensembles_facts
78 cic:/Coq/Sets/Constructive_sets/Ensembles_facts/U.var
81 inline procedural "cic:/Coq/Sets/Constructive_sets/Extension.con" as lemma.
83 inline procedural "cic:/Coq/Sets/Constructive_sets/Noone_in_empty.con" as lemma.
86 Hint Resolve Noone_in_empty.
89 inline procedural "cic:/Coq/Sets/Constructive_sets/Included_Empty.con" as lemma.
92 Hint Resolve Included_Empty.
95 inline procedural "cic:/Coq/Sets/Constructive_sets/Add_intro1.con" as lemma.
98 Hint Resolve Add_intro1.
101 inline procedural "cic:/Coq/Sets/Constructive_sets/Add_intro2.con" as lemma.
104 Hint Resolve Add_intro2.
107 inline procedural "cic:/Coq/Sets/Constructive_sets/Inhabited_add.con" as lemma.
110 Hint Resolve Inhabited_add.
113 inline procedural "cic:/Coq/Sets/Constructive_sets/Inhabited_not_empty.con" as lemma.
116 Hint Resolve Inhabited_not_empty.
119 inline procedural "cic:/Coq/Sets/Constructive_sets/Add_not_Empty.con" as lemma.
122 Hint Resolve Add_not_Empty.
125 inline procedural "cic:/Coq/Sets/Constructive_sets/not_Empty_Add.con" as lemma.
128 Hint Resolve not_Empty_Add.
131 inline procedural "cic:/Coq/Sets/Constructive_sets/Singleton_inv.con" as lemma.
134 Hint Resolve Singleton_inv.
137 inline procedural "cic:/Coq/Sets/Constructive_sets/Singleton_intro.con" as lemma.
140 Hint Resolve Singleton_intro.
143 inline procedural "cic:/Coq/Sets/Constructive_sets/Union_inv.con" as lemma.
145 inline procedural "cic:/Coq/Sets/Constructive_sets/Add_inv.con" as lemma.
147 inline procedural "cic:/Coq/Sets/Constructive_sets/Intersection_inv.con" as lemma.
150 Hint Resolve Intersection_inv.
153 inline procedural "cic:/Coq/Sets/Constructive_sets/Couple_inv.con" as lemma.
156 Hint Resolve Couple_inv.
159 inline procedural "cic:/Coq/Sets/Constructive_sets/Setminus_intro.con" as lemma.
162 Hint Resolve Setminus_intro.
165 inline procedural "cic:/Coq/Sets/Constructive_sets/Strict_Included_intro.con" as lemma.
168 Hint Resolve Strict_Included_intro.
171 inline procedural "cic:/Coq/Sets/Constructive_sets/Strict_Included_strict.con" as lemma.
174 Hint Resolve Strict_Included_strict.
182 Hint Resolve Singleton_inv Singleton_intro Add_intro1 Add_intro2
183 Intersection_inv Couple_inv Setminus_intro Strict_Included_intro
184 Strict_Included_strict Noone_in_empty Inhabited_not_empty Add_not_Empty
185 not_Empty_Add Inhabited_add Included_Empty: sets v62.