Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states par les fichiers nouvelle syntaxe

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5027 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 245 insertions, 241 deletions

diff --git a/theories/Sets/Powerset_Classical_facts.v b/theories/Sets/Powerset_Classical_facts.v
index 6b3443b7d..988bbd25a 100755
--- a/theories/Sets/Powerset_Classical_facts.v
+++ b/theories/Sets/Powerset_Classical_facts.v
@@ -39,300 +39,304 @@ Require Export Classical_sets.
 
 Section Sets_as_an_algebra.
 
-Variable U: Type.
+Variable U : Type.
 
-Lemma sincl_add_x:
-  (A, B: (Ensemble U))
-  (x: U) ~ (In U A x) -> (Strict_Included U (Add U A x) (Add U B x)) ->
-                         (Strict_Included U A B).
+Lemma sincl_add_x :
+ forall (A B:Ensemble U) (x:U),
+   ~ In U A x ->
+   Strict_Included U (Add U A x) (Add U B x) -> Strict_Included U A B.
 Proof.
-Intros A B x H' H'0; Red.
-LApply (Strict_Included_inv U (Add U A x) (Add U B x)); Auto with sets.
-Clear H'0; Intro H'0; Split.
-Apply incl_add_x with x := x; Tauto.
-Elim H'0; Intros H'1 H'2; Elim H'2; Clear H'0 H'2.
-Intros x0 H'0.
-Red; Intro H'2.
-Elim H'0; Clear H'0.
-Rewrite <- H'2; Auto with sets.
+intros A B x H' H'0; red in |- *.
+lapply (Strict_Included_inv U (Add U A x) (Add U B x)); auto with sets.
+clear H'0; intro H'0; split.
+apply incl_add_x with (x := x); tauto.
+elim H'0; intros H'1 H'2; elim H'2; clear H'0 H'2.
+intros x0 H'0.
+red in |- *; intro H'2.
+elim H'0; clear H'0.
+rewrite <- H'2; auto with sets.
 Qed.
 
-Lemma incl_soustr_in:
-  (X: (Ensemble U)) (x: U) (In U X x) -> (Included U (Subtract U X x) X).
+Lemma incl_soustr_in :
+ forall (X:Ensemble U) (x:U), In U X x -> Included U (Subtract U X x) X.
 Proof.
-Intros X x H'; Red.
-Intros x0 H'0; Elim H'0; Auto with sets.
+intros X x H'; red in |- *.
+intros x0 H'0; elim H'0; auto with sets.
 Qed.
-Hints Resolve incl_soustr_in : sets v62.
+Hint Resolve incl_soustr_in: sets v62.
 
-Lemma incl_soustr:
-  (X, Y: (Ensemble U)) (x: U) (Included U X Y) ->
-   (Included U (Subtract U X x) (Subtract U Y x)).
+Lemma incl_soustr :
+ forall (X Y:Ensemble U) (x:U),
+   Included U X Y -> Included U (Subtract U X x) (Subtract U Y x).
 Proof.
-Intros X Y x H'; Red.
-Intros x0 H'0; Elim H'0.
-Intros H'1 H'2.
-Apply Subtract_intro; Auto with sets.
+intros X Y x H'; red in |- *.
+intros x0 H'0; elim H'0.
+intros H'1 H'2.
+apply Subtract_intro; auto with sets.
 Qed.
-Hints Resolve incl_soustr : sets v62.
+Hint Resolve incl_soustr: sets v62.
 
 
-Lemma incl_soustr_add_l:
-  (X: (Ensemble U)) (x: U) (Included U (Subtract U (Add U X x) x) X).
+Lemma incl_soustr_add_l :
+ forall (X:Ensemble U) (x:U), Included U (Subtract U (Add U X x) x) X.
 Proof.
-Intros X x; Red.
-Intros x0 H'; Elim H'; Auto with sets.
-Intro H'0; Elim H'0; Auto with sets.
-Intros t H'1 H'2; Elim H'2; Auto with sets.
+intros X x; red in |- *.
+intros x0 H'; elim H'; auto with sets.
+intro H'0; elim H'0; auto with sets.
+intros t H'1 H'2; elim H'2; auto with sets.
 Qed.
-Hints Resolve incl_soustr_add_l : sets v62.
+Hint Resolve incl_soustr_add_l: sets v62.
 
-Lemma incl_soustr_add_r:
-  (X: (Ensemble U)) (x: U) ~ (In U X x) ->
-   (Included U X (Subtract U (Add U X x) x)).
+Lemma incl_soustr_add_r :
+ forall (X:Ensemble U) (x:U),
+   ~ In U X x -> Included U X (Subtract U (Add U X x) x).
 Proof.
-Intros X x H'; Red.
-Intros x0 H'0; Try Assumption.
-Apply Subtract_intro; Auto with sets.
-Red; Intro H'1; Apply H'; Rewrite H'1; Auto with sets.
+intros X x H'; red in |- *.
+intros x0 H'0; try assumption.
+apply Subtract_intro; auto with sets.
+red in |- *; intro H'1; apply H'; rewrite H'1; auto with sets.
 Qed.
-Hints Resolve incl_soustr_add_r : sets v62.
+Hint Resolve incl_soustr_add_r: sets v62.
 
-Lemma add_soustr_2:
-  (X: (Ensemble U)) (x: U) (In U X x) ->
-   (Included U X (Add U (Subtract U X x) x)).
+Lemma add_soustr_2 :
+ forall (X:Ensemble U) (x:U),
+   In U X x -> Included U X (Add U (Subtract U X x) x).
 Proof.
-Intros X x H'; Red.
-Intros x0 H'0; Try Assumption.
-Elim (classic x == x0); Intro K; Auto with sets.
-Elim K; Auto with sets.
+intros X x H'; red in |- *.
+intros x0 H'0; try assumption.
+elim (classic (x = x0)); intro K; auto with sets.
+elim K; auto with sets.
 Qed.
 
-Lemma add_soustr_1:
-  (X: (Ensemble U)) (x: U) (In U X x) ->
-   (Included U (Add U (Subtract U X x) x) X).
+Lemma add_soustr_1 :
+ forall (X:Ensemble U) (x:U),
+   In U X x -> Included U (Add U (Subtract U X x) x) X.
 Proof.
-Intros X x H'; Red.
-Intros x0 H'0; Elim H'0; Auto with sets.
-Intros y H'1; Elim H'1; Auto with sets.
-Intros t H'1; Try Assumption.
-Rewrite <- (Singleton_inv U x t); Auto with sets.
+intros X x H'; red in |- *.
+intros x0 H'0; elim H'0; auto with sets.
+intros y H'1; elim H'1; auto with sets.
+intros t H'1; try assumption.
+rewrite <- (Singleton_inv U x t); auto with sets.
 Qed.
-Hints Resolve add_soustr_1 add_soustr_2 : sets v62.
+Hint Resolve add_soustr_1 add_soustr_2: sets v62.
 
-Lemma add_soustr_xy:
-  (X: (Ensemble U)) (x, y: U) ~ x == y ->
-    (Subtract U (Add U X x) y) == (Add U (Subtract U X y) x).
+Lemma add_soustr_xy :
+ forall (X:Ensemble U) (x y:U),
+   x <> y -> Subtract U (Add U X x) y = Add U (Subtract U X y) x.
 Proof.
-Intros X x y H'; Apply Extensionality_Ensembles.
-Split; Red.
-Intros x0 H'0; Elim H'0; Auto with sets.
-Intro H'1; Elim H'1.
-Intros u H'2 H'3; Try Assumption.
-Apply Add_intro1.
-Apply Subtract_intro; Auto with sets.
-Intros t H'2 H'3; Try Assumption.
-Elim (Singleton_inv U x t); Auto with sets.
-Intros u H'2; Try Assumption.
-Elim (Add_inv U (Subtract U X y) x u); Auto with sets.
-Intro H'0; Elim H'0; Auto with sets.
-Intro H'0; Rewrite <- H'0; Auto with sets.
+intros X x y H'; apply Extensionality_Ensembles.
+split; red in |- *.
+intros x0 H'0; elim H'0; auto with sets.
+intro H'1; elim H'1.
+intros u H'2 H'3; try assumption.
+apply Add_intro1.
+apply Subtract_intro; auto with sets.
+intros t H'2 H'3; try assumption.
+elim (Singleton_inv U x t); auto with sets.
+intros u H'2; try assumption.
+elim (Add_inv U (Subtract U X y) x u); auto with sets.
+intro H'0; elim H'0; auto with sets.
+intro H'0; rewrite <- H'0; auto with sets.
 Qed.
-Hints Resolve add_soustr_xy : sets v62.
+Hint Resolve add_soustr_xy: sets v62.
 
-Lemma incl_st_add_soustr:
-  (X, Y: (Ensemble U)) (x: U) ~ (In U X x) -> 
-   (Strict_Included U (Add U X x) Y) ->
-   (Strict_Included U X (Subtract U Y x)).
+Lemma incl_st_add_soustr :
+ forall (X Y:Ensemble U) (x:U),
+   ~ In U X x ->
+   Strict_Included U (Add U X x) Y -> Strict_Included U X (Subtract U Y x).
 Proof.
-Intros X Y x H' H'0; Apply sincl_add_x with x := x; Auto with sets.
-Split.
-Elim H'0.
-Intros H'1 H'2.
-Generalize (Inclusion_is_transitive U).
-Intro H'4; Red in H'4.
-Apply H'4 with y := Y; Auto with sets.
-Red in H'0.
-Elim H'0; Intros H'1 H'2; Try Exact H'1; Clear H'0. (* PB *)
-Red; Intro H'0; Apply H'2.
-Rewrite H'0; Auto 8 with sets.
+intros X Y x H' H'0; apply sincl_add_x with (x := x); auto with sets.
+split.
+elim H'0.
+intros H'1 H'2.
+generalize (Inclusion_is_transitive U).
+intro H'4; red in H'4.
+apply H'4 with (y := Y); auto with sets.
+red in H'0.
+elim H'0; intros H'1 H'2; try exact H'1; clear H'0. (* PB *)
+red in |- *; intro H'0; apply H'2.
+rewrite H'0; auto 8 with sets.
 Qed.
 
-Lemma Sub_Add_new:
-  (X: (Ensemble U)) (x: U) ~ (In U X x) -> X == (Subtract U (Add U X x) x).
+Lemma Sub_Add_new :
+ forall (X:Ensemble U) (x:U), ~ In U X x -> X = Subtract U (Add U X x) x.
 Proof.
-Auto with sets.
+auto with sets.
 Qed.
 
-Lemma Simplify_add:
-  (X, X0 : (Ensemble U)) (x: U)
-  ~ (In U X x) -> ~ (In U X0 x) ->  (Add U X x) == (Add U X0 x) -> X == X0.
+Lemma Simplify_add :
+ forall (X X0:Ensemble U) (x:U),
+   ~ In U X x -> ~ In U X0 x -> Add U X x = Add U X0 x -> X = X0.
 Proof.
-Intros X X0 x H' H'0 H'1; Try Assumption.
-Rewrite (Sub_Add_new X x); Auto with sets.
-Rewrite (Sub_Add_new X0 x); Auto with sets.
-Rewrite H'1; Auto with sets.
+intros X X0 x H' H'0 H'1; try assumption.
+rewrite (Sub_Add_new X x); auto with sets.
+rewrite (Sub_Add_new X0 x); auto with sets.
+rewrite H'1; auto with sets.
 Qed.
 
-Lemma Included_Add:
-  (X, A: (Ensemble U)) (x: U) (Included U X (Add U A x)) ->
-   (Included U X A) \/
-   (EXT A' | X == (Add U A' x) /\ (Included U A' A)).
+Lemma Included_Add :
+ forall (X A:Ensemble U) (x:U),
+   Included U X (Add U A x) ->
+   Included U X A \/ ( exists A' : _ | X = Add U A' x /\ Included U A' A).
 Proof.
-Intros X A x H'0; Try Assumption.
-Elim (classic (In U X x)).
-Intro H'1; Right; Try Assumption.
-Exists (Subtract U X x).
-Split; Auto with sets.
-Red in H'0.
-Red.
-Intros x0 H'2; Try Assumption.
-LApply (Subtract_inv U X x x0); Auto with sets.
-Intro H'3; Elim H'3; Intros K K'; Clear H'3.
-LApply (H'0 x0); Auto with sets.
-Intro H'3; Try Assumption.
-LApply (Add_inv U A x x0); Auto with sets.
-Intro H'4; Elim H'4;
- [Intro H'5; Try Exact H'5; Clear H'4 | Intro H'5; Clear H'4].
-Elim K'; Auto with sets.
-Intro H'1; Left; Try Assumption.
-Red in H'0.
-Red.
-Intros x0 H'2; Try Assumption.
-LApply (H'0 x0); Auto with sets.
-Intro H'3; Try Assumption.
-LApply (Add_inv U A x x0); Auto with sets.
-Intro H'4; Elim H'4;
- [Intro H'5; Try Exact H'5; Clear H'4 | Intro H'5; Clear H'4].
-Absurd (In U X x0); Auto with sets.
-Rewrite <- H'5; Auto with sets.
+intros X A x H'0; try assumption.
+elim (classic (In U X x)).
+intro H'1; right; try assumption.
+exists (Subtract U X x).
+split; auto with sets.
+red in H'0.
+red in |- *.
+intros x0 H'2; try assumption.
+lapply (Subtract_inv U X x x0); auto with sets.
+intro H'3; elim H'3; intros K K'; clear H'3.
+lapply (H'0 x0); auto with sets.
+intro H'3; try assumption.
+lapply (Add_inv U A x x0); auto with sets.
+intro H'4; elim H'4;
+ [ intro H'5; try exact H'5; clear H'4 | intro H'5; clear H'4 ].
+elim K'; auto with sets.
+intro H'1; left; try assumption.
+red in H'0.
+red in |- *.
+intros x0 H'2; try assumption.
+lapply (H'0 x0); auto with sets.
+intro H'3; try assumption.
+lapply (Add_inv U A x x0); auto with sets.
+intro H'4; elim H'4;
+ [ intro H'5; try exact H'5; clear H'4 | intro H'5; clear H'4 ].
+absurd (In U X x0); auto with sets.
+rewrite <- H'5; auto with sets.
 Qed.
 
-Lemma setcover_inv:
- (A: (Ensemble U))
- (x, y: (Ensemble U)) (covers (Ensemble U) (Power_set_PO U A) y x) ->
- (Strict_Included U x y) /\
- ((z: (Ensemble U)) (Included U x z) -> (Included U z y) -> x == z \/ z == y).
+Lemma setcover_inv :
+ forall A x y:Ensemble U,
+   covers (Ensemble U) (Power_set_PO U A) y x ->
+   Strict_Included U x y /\
+   (forall z:Ensemble U, Included U x z -> Included U z y -> x = z \/ z = y).
 Proof.
-Intros A x y H'; Elim H'.
-Unfold Strict_Rel_of; Simpl.
-Intros H'0 H'1; Split; [Auto with sets | Idtac].
-Intros z H'2 H'3; Try Assumption.
-Elim (classic  x == z); Auto with sets.
-Intro H'4; Right; Try Assumption.
-Elim (classic  z == y); Auto with sets.
-Intro H'5; Try Assumption.
-Elim H'1.
-Exists z; Auto with sets.
+intros A x y H'; elim H'.
+unfold Strict_Rel_of in |- *; simpl in |- *.
+intros H'0 H'1; split; [ auto with sets | idtac ].
+intros z H'2 H'3; try assumption.
+elim (classic (x = z)); auto with sets.
+intro H'4; right; try assumption.
+elim (classic (z = y)); auto with sets.
+intro H'5; try assumption.
+elim H'1.
+exists z; auto with sets.
 Qed.
 
-Theorem Add_covers:
-  (A: (Ensemble U)) (a: (Ensemble U)) (Included U a A) ->
-   (x: U) (In U A x) -> ~ (In U a x) ->
-    (covers (Ensemble U) (Power_set_PO U A) (Add U a x) a).
+Theorem Add_covers :
+ forall A a:Ensemble U,
+   Included U a A ->
+   forall x:U,
+     In U A x ->
+     ~ In U a x -> covers (Ensemble U) (Power_set_PO U A) (Add U a x) a.
 Proof.
-Intros A a H' x H'0 H'1; Try Assumption.
-Apply setcover_intro; Auto with sets.
-Red.
-Split; [Idtac | Red; Intro H'2; Try Exact H'2]; Auto with sets.
-Apply H'1.
-Rewrite H'2; Auto with sets.
-Red; Intro H'2; Elim H'2; Clear H'2.
-Intros z H'2; Elim H'2; Intros H'3 H'4; Try Exact H'3; Clear H'2.
-LApply (Strict_Included_inv U a z); Auto with sets; Clear H'3.
-Intro H'2; Elim H'2; Intros H'3 H'5; Elim H'5; Clear H'2 H'5.
-Intros x0 H'2; Elim H'2.
-Intros H'5 H'6; Try Assumption.
-Generalize H'4; Intro K.
-Red in H'4.
-Elim H'4; Intros H'8 H'9; Red in H'8; Clear H'4.
-LApply (H'8 x0); Auto with sets.
-Intro H'7; Try Assumption.
-Elim (Add_inv U a x x0); Auto with sets.
-Intro H'15.
-Cut (Included U (Add U a x) z).
-Intro H'10; Try Assumption.
-Red in K.
-Elim K; Intros H'11 H'12; Apply H'12; Clear K; Auto with sets.
-Rewrite H'15.
-Red.
-Intros x1 H'10; Elim H'10; Auto with sets.
-Intros x2 H'11; Elim H'11; Auto with sets.
+intros A a H' x H'0 H'1; try assumption.
+apply setcover_intro; auto with sets.
+red in |- *.
+split; [ idtac | red in |- *; intro H'2; try exact H'2 ]; auto with sets.
+apply H'1.
+rewrite H'2; auto with sets.
+red in |- *; intro H'2; elim H'2; clear H'2.
+intros z H'2; elim H'2; intros H'3 H'4; try exact H'3; clear H'2.
+lapply (Strict_Included_inv U a z); auto with sets; clear H'3.
+intro H'2; elim H'2; intros H'3 H'5; elim H'5; clear H'2 H'5.
+intros x0 H'2; elim H'2.
+intros H'5 H'6; try assumption.
+generalize H'4; intro K.
+red in H'4.
+elim H'4; intros H'8 H'9; red in H'8; clear H'4.
+lapply (H'8 x0); auto with sets.
+intro H'7; try assumption.
+elim (Add_inv U a x x0); auto with sets.
+intro H'15.
+cut (Included U (Add U a x) z).
+intro H'10; try assumption.
+red in K.
+elim K; intros H'11 H'12; apply H'12; clear K; auto with sets.
+rewrite H'15.
+red in |- *.
+intros x1 H'10; elim H'10; auto with sets.
+intros x2 H'11; elim H'11; auto with sets.
 Qed.
 
-Theorem covers_Add:
-  (A: (Ensemble U))
-  (a, a': (Ensemble U))
-  (Included U a A) ->
-  (Included U a' A) -> (covers (Ensemble U) (Power_set_PO U A) a' a) ->
-   (EXT x | a' == (Add U a x) /\ ((In U A x) /\ ~ (In U a x))).
+Theorem covers_Add :
+ forall A a a':Ensemble U,
+   Included U a A ->
+   Included U a' A ->
+   covers (Ensemble U) (Power_set_PO U A) a' a ->
+    exists x : _ | a' = Add U a x /\ In U A x /\ ~ In U a x.
 Proof.
-Intros A a a' H' H'0 H'1; Try Assumption.
-Elim (setcover_inv A a a'); Auto with sets.
-Intros H'6 H'7.
-Clear H'1.
-Elim (Strict_Included_inv U a a'); Auto with sets.
-Intros H'5 H'8; Elim H'8.
-Intros x H'1; Elim H'1.
-Intros H'2 H'3; Try Assumption.
-Exists x.
-Split; [Try Assumption | Idtac].
-Clear H'8 H'1.
-Elim (H'7 (Add U a x)); Auto with sets.
-Intro H'1.
-Absurd a ==(Add U a x); Auto with sets.
-Red; Intro H'8; Try Exact H'8.
-Apply H'3.
-Rewrite H'8; Auto with sets.
-Auto with sets.
-Red.
-Intros x0 H'1; Elim H'1; Auto with sets.
-Intros x1 H'8; Elim H'8; Auto with sets.
-Split; [Idtac | Try Assumption].
-Red in H'0; Auto with sets.
+intros A a a' H' H'0 H'1; try assumption.
+elim (setcover_inv A a a'); auto with sets.
+intros H'6 H'7.
+clear H'1.
+elim (Strict_Included_inv U a a'); auto with sets.
+intros H'5 H'8; elim H'8.
+intros x H'1; elim H'1.
+intros H'2 H'3; try assumption.
+exists x.
+split; [ try assumption | idtac ].
+clear H'8 H'1.
+elim (H'7 (Add U a x)); auto with sets.
+intro H'1.
+absurd (a = Add U a x); auto with sets.
+red in |- *; intro H'8; try exact H'8.
+apply H'3.
+rewrite H'8; auto with sets.
+auto with sets.
+red in |- *.
+intros x0 H'1; elim H'1; auto with sets.
+intros x1 H'8; elim H'8; auto with sets.
+split; [ idtac | try assumption ].
+red in H'0; auto with sets.
 Qed.
 
-Theorem covers_is_Add:
-  (A: (Ensemble U))
-  (a, a': (Ensemble U)) (Included U a A) -> (Included U a' A) ->
-   (iff
-      (covers (Ensemble U) (Power_set_PO U A) a' a)
-      (EXT x | a' == (Add U a x) /\ ((In U A x) /\ ~ (In U a x)))).
+Theorem covers_is_Add :
+ forall A a a':Ensemble U,
+   Included U a A ->
+   Included U a' A ->
+   (covers (Ensemble U) (Power_set_PO U A) a' a <->
+    ( exists x : _ | a' = Add U a x /\ In U A x /\ ~ In U a x)).
 Proof.
-Intros A a a' H' H'0; Split; Intro K.
-Apply covers_Add with A := A; Auto with sets.
-Elim K.
-Intros x H'1; Elim H'1; Intros H'2 H'3; Rewrite H'2; Clear H'1.
-Apply Add_covers; Intuition.
+intros A a a' H' H'0; split; intro K.
+apply covers_Add with (A := A); auto with sets.
+elim K.
+intros x H'1; elim H'1; intros H'2 H'3; rewrite H'2; clear H'1.
+apply Add_covers; intuition.
 Qed.
 
-Theorem Singleton_atomic:
-  (x:U) (A:(Ensemble U)) (In U A x) ->
-  (covers (Ensemble U) (Power_set_PO U A) (Singleton U x) (Empty_set U)).
-Intros x A H'.
-Rewrite <- (Empty_set_zero' U x).
-Apply Add_covers; Auto with sets.
+Theorem Singleton_atomic :
+ forall (x:U) (A:Ensemble U),
+   In U A x ->
+   covers (Ensemble U) (Power_set_PO U A) (Singleton U x) (Empty_set U).
+intros x A H'.
+rewrite <- (Empty_set_zero' U x).
+apply Add_covers; auto with sets.
 Qed.
 
-Lemma less_than_singleton:
-  (X:(Ensemble U)) (x:U) (Strict_Included U X (Singleton U x)) ->
-  X ==(Empty_set U).
-Intros X x H'; Try Assumption.
-Red in H'.
-LApply (Singleton_atomic x (Full_set U));
- [Intro H'2; Try Exact H'2 | Apply Full_intro].
-Elim H'; Intros H'0 H'1; Try Exact H'1; Clear H'.
-Elim (setcover_inv (Full_set U) (Empty_set U) (Singleton U x));
- [Intros H'6 H'7; Try Exact H'7 | Idtac]; Auto with sets.
-Elim (H'7 X); [Intro H'5; Try Exact H'5 | Intro H'5 | Idtac | Idtac]; Auto with sets.
-Elim H'1; Auto with sets.
+Lemma less_than_singleton :
+ forall (X:Ensemble U) (x:U),
+   Strict_Included U X (Singleton U x) -> X = Empty_set U.
+intros X x H'; try assumption.
+red in H'.
+lapply (Singleton_atomic x (Full_set U));
+ [ intro H'2; try exact H'2 | apply Full_intro ].
+elim H'; intros H'0 H'1; try exact H'1; clear H'.
+elim (setcover_inv (Full_set U) (Empty_set U) (Singleton U x));
+ [ intros H'6 H'7; try exact H'7 | idtac ]; auto with sets.
+elim (H'7 X); [ intro H'5; try exact H'5 | intro H'5 | idtac | idtac ];
+ auto with sets.
+elim H'1; auto with sets.
 Qed.
 
 End Sets_as_an_algebra.
 
-Hints Resolve incl_soustr_in : sets v62.
-Hints Resolve incl_soustr : sets v62.
-Hints Resolve incl_soustr_add_l : sets v62.
-Hints Resolve incl_soustr_add_r : sets v62.
-Hints Resolve add_soustr_1 add_soustr_2 : sets v62.
-Hints Resolve add_soustr_xy : sets v62.
+Hint Resolve incl_soustr_in: sets v62.
+Hint Resolve incl_soustr: sets v62.
+Hint Resolve incl_soustr_add_l: sets v62.
+Hint Resolve incl_soustr_add_r: sets v62.
+Hint Resolve add_soustr_1 add_soustr_2: sets v62.
+Hint Resolve add_soustr_xy: sets v62.
\ No newline at end of file