diff options
Diffstat (limited to 'theories/Sets/Constructive_sets.v')
| -rw-r--r-- | theories/Sets/Constructive_sets.v | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/theories/Sets/Constructive_sets.v b/theories/Sets/Constructive_sets.v index ad81316d..0719365f 100644 --- a/theories/Sets/Constructive_sets.v +++ b/theories/Sets/Constructive_sets.v @@ -24,13 +24,13 @@ (* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) (****************************************************************************) -(*i $Id: Constructive_sets.v 9245 2006-10-17 12:53:34Z notin $ i*) +(*i $Id$ i*) Require Export Ensembles. Section Ensembles_facts. Variable U : Type. - + Lemma Extension : forall B C:Ensemble U, B = C -> Same_set U B C. Proof. intros B C H'; rewrite H'; auto with sets. @@ -52,7 +52,7 @@ Section Ensembles_facts. Proof. unfold Add at 1 in |- *; auto with sets. Qed. - + Lemma Add_intro2 : forall (A:Ensemble U) (x:U), In U (Add U A x) x. Proof. unfold Add at 1 in |- *; auto with sets. @@ -98,15 +98,15 @@ Section Ensembles_facts. Proof. intros B C x H'; elim H'; auto with sets. Qed. - + Lemma Add_inv : forall (A:Ensemble U) (x y:U), In U (Add U A x) y -> In U A y \/ x = y. Proof. - intros A x y H'; induction H'. + intros A x y H'; induction H'. left; assumption. right; apply Singleton_inv; assumption. Qed. - + Lemma Intersection_inv : forall (B C:Ensemble U) (x:U), In U (Intersection U B C) x -> In U B x /\ In U C x. @@ -125,7 +125,7 @@ Section Ensembles_facts. Proof. unfold Setminus at 1 in |- *; red in |- *; auto with sets. Qed. - + Lemma Strict_Included_intro : forall X Y:Ensemble U, Included U X Y /\ X <> Y -> Strict_Included U X Y. Proof. |