-(*i $Id: Setoid.v,v 1.5 2003/11/29 17:28:41 herbelin Exp $: i*)
+(*#***********************************************************************)
+
+(*i $Id: Setoid.v,v 1.5.2.1 2004/07/16 19:31:17 herbelin Exp $: i*)
inline procedural "cic:/Coq/Setoids/Setoid/or_ext1.con" as theorem.
inline procedural "cic:/Coq/Setoids/Setoid/or_ext2.con" as theorem.
inline procedural "cic:/Coq/Setoids/Setoid/or_ext1.con" as theorem.
inline procedural "cic:/Coq/Setoids/Setoid/or_ext2.con" as theorem.
inline procedural "cic:/Coq/Setoids/Setoid/and_ext1.con" as theorem.
inline procedural "cic:/Coq/Setoids/Setoid/and_ext2.con" as theorem.
inline procedural "cic:/Coq/Setoids/Setoid/and_ext1.con" as theorem.
inline procedural "cic:/Coq/Setoids/Setoid/and_ext2.con" as theorem.
inline procedural "cic:/Coq/Setoids/Setoid/not_ext1.con" as theorem.
inline procedural "cic:/Coq/Setoids/Setoid/not_ext2.con" as theorem.
inline procedural "cic:/Coq/Setoids/Setoid/fleche.con" as definition.
inline procedural "cic:/Coq/Setoids/Setoid/not_ext1.con" as theorem.
inline procedural "cic:/Coq/Setoids/Setoid/not_ext2.con" as theorem.
inline procedural "cic:/Coq/Setoids/Setoid/fleche.con" as definition.
inline procedural "cic:/Coq/Setoids/Setoid/fleche_ext1.con" as theorem.
inline procedural "cic:/Coq/Setoids/Setoid/fleche_ext2.con" as theorem.
inline procedural "cic:/Coq/Setoids/Setoid/fleche_ext1.con" as theorem.
inline procedural "cic:/Coq/Setoids/Setoid/fleche_ext2.con" as theorem.