(**************************************************************************)
(*       ___                                                              *)
(*      ||M||                                                             *)
(*      ||A||       A project by Andrea Asperti                           *)
(*      ||T||                                                             *)
(*      ||I||       Developers:                                           *)
(*      ||T||         The HELM team.                                      *)
(*      ||A||         http://helm.cs.unibo.it                             *)
(*      \   /                                                             *)
(*       \ /        This file is distributed under the terms of the       *)
(*        v         GNU General Public License Version 2                  *)
(*                                                                        *)
(**************************************************************************)

(* This file was automatically generated: do not edit *********************)

include "Coq.ma".

include "Init/Prelude.ma".

(*#***********************************************************************)

(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)

(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)

(*   \VV/  **************************************************************)

(*    //   *      This file is distributed under the terms of the       *)

(*         *       GNU Lesser General Public License Version 2.1        *)

(*#***********************************************************************)

(*#***************************************************************************)

(*                                                                          *)

(*                         Naive Set Theory in Coq                          *)

(*                                                                          *)

(*                     INRIA                        INRIA                   *)

(*              Rocquencourt                        Sophia-Antipolis        *)

(*                                                                          *)

(*                                 Coq V6.1                                 *)

(*									    *)

(*			         Gilles Kahn 				    *)

(*				 Gerard Huet				    *)

(*									    *)

(*									    *)

(*                                                                          *)

(* Acknowledgments: This work was started in July 1993 by F. Prost. Thanks  *)

(* to the Newton Institute for providing an exceptional work environment    *)

(* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)

(*#***************************************************************************)

(*i $Id: Ensembles.v,v 1.7.2.1 2004/07/16 19:31:17 herbelin Exp $ i*)

(* UNEXPORTED
Section Ensembles
*)

(* UNEXPORTED
cic:/Coq/Sets/Ensembles/Ensembles/U.var
*)

inline procedural "cic:/Coq/Sets/Ensembles/Ensemble.con" as definition.

inline procedural "cic:/Coq/Sets/Ensembles/In.con" as definition.

inline procedural "cic:/Coq/Sets/Ensembles/Included.con" as definition.

inline procedural "cic:/Coq/Sets/Ensembles/Empty_set.ind".

inline procedural "cic:/Coq/Sets/Ensembles/Full_set.ind".

(*#* NB: The following definition builds-in equality of elements in [U] as 
   Leibniz equality. 

   This may have to be changed if we replace [U] by a Setoid on [U] 
   with its own equality [eqs], with  
   [In_singleton: (y: U)(eqs x y) -> (In (Singleton x) y)]. *)

inline procedural "cic:/Coq/Sets/Ensembles/Singleton.ind".

inline procedural "cic:/Coq/Sets/Ensembles/Union.ind".

inline procedural "cic:/Coq/Sets/Ensembles/Add.con" as definition.

inline procedural "cic:/Coq/Sets/Ensembles/Intersection.ind".

inline procedural "cic:/Coq/Sets/Ensembles/Couple.ind".

inline procedural "cic:/Coq/Sets/Ensembles/Triple.ind".

inline procedural "cic:/Coq/Sets/Ensembles/Complement.con" as definition.

inline procedural "cic:/Coq/Sets/Ensembles/Setminus.con" as definition.

inline procedural "cic:/Coq/Sets/Ensembles/Subtract.con" as definition.

inline procedural "cic:/Coq/Sets/Ensembles/Disjoint.ind".

inline procedural "cic:/Coq/Sets/Ensembles/Inhabited.ind".

inline procedural "cic:/Coq/Sets/Ensembles/Strict_Included.con" as definition.

inline procedural "cic:/Coq/Sets/Ensembles/Same_set.con" as definition.

(*#* Extensionality Axiom *)

inline procedural "cic:/Coq/Sets/Ensembles/Extensionality_Ensembles.con".

(* UNEXPORTED
Hint Resolve Extensionality_Ensembles.
*)

(* UNEXPORTED
End Ensembles
*)

(* UNEXPORTED
Hint Unfold In Included Same_set Strict_Included Add Setminus Subtract: sets
  v62.
*)

(* UNEXPORTED
Hint Resolve Union_introl Union_intror Intersection_intro In_singleton
  Couple_l Couple_r Triple_l Triple_m Triple_r Disjoint_intro
  Extensionality_Ensembles: sets v62.
*)