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, 250 insertions, 248 deletions

diff --git a/theories/Sets/Finite_sets_facts.v b/theories/Sets/Finite_sets_facts.v
index 4e7b6931f..2849bce6c 100755
--- a/theories/Sets/Finite_sets_facts.v
+++ b/theories/Sets/Finite_sets_facts.v
@@ -37,309 +37,311 @@ Require Export Gt.
 Require Export Lt.
 
 Section Finite_sets_facts.
-Variable U: Type.
+Variable U : Type.
 
 Lemma finite_cardinal :
- (X: (Ensemble U)) (Finite U X) -> (EX n:nat |(cardinal U X n)).
+ forall X:Ensemble U, Finite U X ->  exists n : nat | cardinal U X n.
 Proof.
-NewInduction 1 as [|A _ [n H]].
-Exists O; Auto with sets.
-Exists (S n); Auto with sets.
+induction 1 as [| A _ [n H]].
+exists 0; auto with sets.
+exists (S n); auto with sets.
 Qed.
 
-Lemma cardinal_finite:
-  (X: (Ensemble U)) (n: nat) (cardinal U X n) -> (Finite U X).
+Lemma cardinal_finite :
+ forall (X:Ensemble U) (n:nat), cardinal U X n -> Finite U X.
 Proof.
-NewInduction 1; Auto with sets.
+induction 1; auto with sets.
 Qed.
 
-Theorem Add_preserves_Finite:
-  (X: (Ensemble U)) (x: U) (Finite U X) -> (Finite U (Add U X x)).
+Theorem Add_preserves_Finite :
+ forall (X:Ensemble U) (x:U), Finite U X -> Finite U (Add U X x).
 Proof.
-Intros X x H'.
-Elim (classic (In U X x)); Intro H'0; Auto with sets.
-Rewrite (Non_disjoint_union U X x); Auto with sets.
+intros X x H'.
+elim (classic (In U X x)); intro H'0; auto with sets.
+rewrite (Non_disjoint_union U X x); auto with sets.
 Qed.
-Hints Resolve Add_preserves_Finite.
+Hint Resolve Add_preserves_Finite.
 
-Theorem Singleton_is_finite: (x: U) (Finite U (Singleton U x)).
+Theorem Singleton_is_finite : forall x:U, Finite U (Singleton U x).
 Proof.
-Intro x; Rewrite <- (Empty_set_zero U (Singleton U x)).
-Change (Finite U (Add U (Empty_set U) x)); Auto with sets.
+intro x; rewrite <- (Empty_set_zero U (Singleton U x)).
+change (Finite U (Add U (Empty_set U) x)) in |- *; auto with sets.
 Qed.
-Hints Resolve Singleton_is_finite.
+Hint Resolve Singleton_is_finite.
 
-Theorem Union_preserves_Finite:
-  (X, Y: (Ensemble U)) (Finite U X) -> (Finite U Y) -> 
-                       (Finite U (Union U X Y)).
+Theorem Union_preserves_Finite :
+ forall X Y:Ensemble U, Finite U X -> Finite U Y -> Finite U (Union U X Y).
 Proof.
-Intros X Y H'; Elim H'.
-Rewrite (Empty_set_zero U Y); Auto with sets.
-Intros A H'0 H'1 x H'2 H'3.
-Rewrite (Union_commutative U (Add U A x) Y).
-Rewrite <- (Union_add U Y A x).
-Rewrite (Union_commutative U Y A); Auto with sets.
+intros X Y H'; elim H'.
+rewrite (Empty_set_zero U Y); auto with sets.
+intros A H'0 H'1 x H'2 H'3.
+rewrite (Union_commutative U (Add U A x) Y).
+rewrite <- (Union_add U Y A x).
+rewrite (Union_commutative U Y A); auto with sets.
 Qed.
 
-Lemma Finite_downward_closed:
-  (A: (Ensemble U)) (Finite U A) ->
-   (X: (Ensemble U)) (Included U X A) -> (Finite U X).
+Lemma Finite_downward_closed :
+ forall A:Ensemble U,
+   Finite U A -> forall X:Ensemble U, Included U X A -> Finite U X.
 Proof.
-Intros A H'; Elim H'; Auto with sets.
-Intros X H'0.
-Rewrite (less_than_empty U X H'0); Auto with sets.
-Intros; Elim Included_Add with U X A0 x; Auto with sets.
-NewDestruct 1 as [A' [H5 H6]].
-Rewrite H5; Auto with sets.
+intros A H'; elim H'; auto with sets.
+intros X H'0.
+rewrite (less_than_empty U X H'0); auto with sets.
+intros; elim Included_Add with U X A0 x; auto with sets.
+destruct 1 as [A' [H5 H6]].
+rewrite H5; auto with sets.
 Qed.
 
-Lemma Intersection_preserves_finite:
-  (A: (Ensemble U)) (Finite U A) ->
-   (X: (Ensemble U)) (Finite U (Intersection U X A)).
+Lemma Intersection_preserves_finite :
+ forall A:Ensemble U,
+   Finite U A -> forall X:Ensemble U, Finite U (Intersection U X A).
 Proof.
-Intros A H' X; Apply Finite_downward_closed with A; Auto with sets.
+intros A H' X; apply Finite_downward_closed with A; auto with sets.
 Qed.
 
-Lemma cardinalO_empty:
-  (X: (Ensemble U)) (cardinal U X O) -> X == (Empty_set U).
+Lemma cardinalO_empty :
+ forall X:Ensemble U, cardinal U X 0 -> X = Empty_set U.
 Proof.
-Intros X H; Apply (cardinal_invert U X O); Trivial with sets.
+intros X H; apply (cardinal_invert U X 0); trivial with sets.
 Qed.
-Hints Resolve cardinalO_empty.
+Hint Resolve cardinalO_empty.
 
-Lemma inh_card_gt_O:
-  (X: (Ensemble U)) (Inhabited U X) -> (n: nat) (cardinal U X n) -> (gt n O).
+Lemma inh_card_gt_O :
+ forall X:Ensemble U, Inhabited U X -> forall n:nat, cardinal U X n -> n > 0.
 Proof.
-NewInduction 1 as [x H'].
-Intros n H'0.
-Elim (gt_O_eq n); Auto with sets.
-Intro H'1; Generalize H'; Generalize H'0.
-Rewrite <- H'1; Intro H'2.
-Rewrite (cardinalO_empty X); Auto with sets.
-Intro H'3; Elim H'3.
+induction 1 as [x H'].
+intros n H'0.
+elim (gt_O_eq n); auto with sets.
+intro H'1; generalize H'; generalize H'0.
+rewrite <- H'1; intro H'2.
+rewrite (cardinalO_empty X); auto with sets.
+intro H'3; elim H'3.
 Qed.
 
-Lemma card_soustr_1:
-  (X: (Ensemble U)) (n: nat) (cardinal U X n) ->
-   (x: U) (In U X x) -> (cardinal U (Subtract U X x) (pred n)).
+Lemma card_soustr_1 :
+ forall (X:Ensemble U) (n:nat),
+   cardinal U X n ->
+   forall x:U, In U X x -> cardinal U (Subtract U X x) (pred n).
 Proof.
-Intros X n H'; Elim H'.
-Intros x H'0; Elim H'0.
-Clear H' n X.
-Intros X n H' H'0 x H'1 x0 H'2.
-Elim (classic (In U X x0)).
-Intro H'4; Rewrite (add_soustr_xy U X x x0).
-Elim (classic x == x0).
-Intro H'5.
-Absurd (In U X x0); Auto with sets.
-Rewrite <- H'5; Auto with sets.
-Intro H'3; Try Assumption.
-Cut (S (pred n)) = (pred (S n)).
-Intro H'5; Rewrite <- H'5.
-Apply card_add; Auto with sets.
-Red; Intro H'6; Elim H'6.
-Intros H'7 H'8; Try Assumption.
-Elim H'1; Auto with sets.
-Unfold 2 pred; Symmetry.
-Apply S_pred with m := O.
-Change (gt n O).
-Apply inh_card_gt_O with X := X; Auto with sets.
-Apply Inhabited_intro with x := x0; Auto with sets.
-Red; Intro H'3.
-Apply H'1.
-Elim H'3; Auto with sets.
-Rewrite H'3; Auto with sets.
-Elim (classic x == x0).
-Intro H'3; Rewrite <- H'3.
-Cut (Subtract U (Add U X x) x) == X; Auto with sets.
-Intro H'4; Rewrite H'4; Auto with sets.
-Intros H'3 H'4; Try Assumption.
-Absurd (In U (Add U X x) x0); Auto with sets.
-Red; Intro H'5; Try Exact H'5.
-LApply (Add_inv U X x x0); Tauto.
+intros X n H'; elim H'.
+intros x H'0; elim H'0.
+clear H' n X.
+intros X n H' H'0 x H'1 x0 H'2.
+elim (classic (In U X x0)).
+intro H'4; rewrite (add_soustr_xy U X x x0).
+elim (classic (x = x0)).
+intro H'5.
+absurd (In U X x0); auto with sets.
+rewrite <- H'5; auto with sets.
+intro H'3; try assumption.
+cut (S (pred n) = pred (S n)).
+intro H'5; rewrite <- H'5.
+apply card_add; auto with sets.
+red in |- *; intro H'6; elim H'6.
+intros H'7 H'8; try assumption.
+elim H'1; auto with sets.
+unfold pred at 2 in |- *; symmetry  in |- *.
+apply S_pred with (m := 0).
+change (n > 0) in |- *.
+apply inh_card_gt_O with (X := X); auto with sets.
+apply Inhabited_intro with (x := x0); auto with sets.
+red in |- *; intro H'3.
+apply H'1.
+elim H'3; auto with sets.
+rewrite H'3; auto with sets.
+elim (classic (x = x0)).
+intro H'3; rewrite <- H'3.
+cut (Subtract U (Add U X x) x = X); auto with sets.
+intro H'4; rewrite H'4; auto with sets.
+intros H'3 H'4; try assumption.
+absurd (In U (Add U X x) x0); auto with sets.
+red in |- *; intro H'5; try exact H'5.
+lapply (Add_inv U X x x0); tauto.
 Qed.
 
-Lemma cardinal_is_functional:
-  (X: (Ensemble U)) (c1: nat) (cardinal U X c1) ->
-   (Y: (Ensemble U)) (c2: nat) (cardinal U Y c2) -> X == Y ->
-    c1 = c2.
+Lemma cardinal_is_functional :
+ forall (X:Ensemble U) (c1:nat),
+   cardinal U X c1 ->
+   forall (Y:Ensemble U) (c2:nat), cardinal U Y c2 -> X = Y -> c1 = c2.
 Proof.
-Intros X c1 H'; Elim H'.
-Intros Y c2 H'0; Elim H'0; Auto with sets.
-Intros A n H'1 H'2 x H'3 H'5.
-Elim (not_Empty_Add U A x); Auto with sets.
-Clear H' c1 X.
-Intros X n H' H'0 x H'1 Y c2 H'2.
-Elim H'2.
-Intro H'3.
-Elim (not_Empty_Add U X x); Auto with sets.
-Clear H'2 c2 Y.
-Intros X0 c2 H'2 H'3 x0 H'4 H'5.
-Elim (classic (In U X0 x)).
-Intro H'6; Apply f_equal with nat.
-Apply H'0 with Y := (Subtract U (Add U X0 x0) x).
-ElimType (pred (S c2)) = c2; Auto with sets.
-Apply card_soustr_1; Auto with sets.
-Rewrite <- H'5.
-Apply Sub_Add_new; Auto with sets.
-Elim (classic x == x0).
-Intros H'6 H'7; Apply f_equal with nat.
-Apply H'0 with Y := X0; Auto with sets.
-Apply Simplify_add with x := x; Auto with sets.
-Pattern 2 x; Rewrite H'6; Auto with sets.
-Intros H'6 H'7.
-Absurd (Add U X x) == (Add U X0 x0); Auto with sets.
-Clear H'0 H' H'3 n H'5 H'4 H'2 H'1 c2.
-Red; Intro H'.
-LApply (Extension U (Add U X x) (Add U X0 x0)); Auto with sets.
-Clear H'.
-Intro H'; Red in H'.
-Elim H'; Intros H'0 H'1; Red in H'0; Clear H' H'1.
-Absurd (In U (Add U X0 x0) x); Auto with sets.
-LApply (Add_inv U X0 x0 x); [ Intuition | Apply (H'0 x); Apply Add_intro2 ].
+intros X c1 H'; elim H'.
+intros Y c2 H'0; elim H'0; auto with sets.
+intros A n H'1 H'2 x H'3 H'5.
+elim (not_Empty_Add U A x); auto with sets.
+clear H' c1 X.
+intros X n H' H'0 x H'1 Y c2 H'2.
+elim H'2.
+intro H'3.
+elim (not_Empty_Add U X x); auto with sets.
+clear H'2 c2 Y.
+intros X0 c2 H'2 H'3 x0 H'4 H'5.
+elim (classic (In U X0 x)).
+intro H'6; apply f_equal with nat.
+apply H'0 with (Y := Subtract U (Add U X0 x0) x).
+elimtype (pred (S c2) = c2); auto with sets.
+apply card_soustr_1; auto with sets.
+rewrite <- H'5.
+apply Sub_Add_new; auto with sets.
+elim (classic (x = x0)).
+intros H'6 H'7; apply f_equal with nat.
+apply H'0 with (Y := X0); auto with sets.
+apply Simplify_add with (x := x); auto with sets.
+pattern x at 2 in |- *; rewrite H'6; auto with sets.
+intros H'6 H'7.
+absurd (Add U X x = Add U X0 x0); auto with sets.
+clear H'0 H' H'3 n H'5 H'4 H'2 H'1 c2.
+red in |- *; intro H'.
+lapply (Extension U (Add U X x) (Add U X0 x0)); auto with sets.
+clear H'.
+intro H'; red in H'.
+elim H'; intros H'0 H'1; red in H'0; clear H' H'1.
+absurd (In U (Add U X0 x0) x); auto with sets.
+lapply (Add_inv U X0 x0 x); [ intuition | apply (H'0 x); apply Add_intro2 ].
 Qed.
 
-Lemma cardinal_Empty : (m:nat)(cardinal U (Empty_set U) m) -> O = m.
+Lemma cardinal_Empty : forall m:nat, cardinal U (Empty_set U) m -> 0 = m.
 Proof.
-Intros m Cm; Generalize (cardinal_invert U (Empty_set U) m Cm).
-Elim m; Auto with sets.
-Intros; Elim H0; Intros; Elim H1; Intros; Elim H2; Intros.
-Elim (not_Empty_Add U x x0 H3).
+intros m Cm; generalize (cardinal_invert U (Empty_set U) m Cm).
+elim m; auto with sets.
+intros; elim H0; intros; elim H1; intros; elim H2; intros.
+elim (not_Empty_Add U x x0 H3).
 Qed.
 
 Lemma cardinal_unicity :
-  (X: (Ensemble U)) (n: nat) (cardinal U X n) -> 
-                    (m: nat) (cardinal U X m) -> n = m.
+ forall (X:Ensemble U) (n:nat),
+   cardinal U X n -> forall m:nat, cardinal U X m -> n = m.
 Proof.
-Intros; Apply cardinal_is_functional with X X; Auto with sets.
+intros; apply cardinal_is_functional with X X; auto with sets.
 Qed.
 
-Lemma card_Add_gen:
-  (A: (Ensemble U))
-  (x: U) (n, n': nat) (cardinal U A n) -> (cardinal U (Add U A x) n') ->
-   (le n' (S n)).
+Lemma card_Add_gen :
+ forall (A:Ensemble U) (x:U) (n n':nat),
+   cardinal U A n -> cardinal U (Add U A x) n' -> n' <= S n.
 Proof.
-Intros A x n n' H'.
-Elim (classic (In U A x)).
-Intro H'0.
-Rewrite (Non_disjoint_union U A x H'0).
-Intro H'1; Cut n = n'.
-Intro E; Rewrite E; Auto with sets.
-Apply cardinal_unicity with A; Auto with sets.
-Intros H'0 H'1.
-Cut n'=(S n).
-Intro E; Rewrite E; Auto with sets.
-Apply cardinal_unicity with (Add U A x); Auto with sets.
+intros A x n n' H'.
+elim (classic (In U A x)).
+intro H'0.
+rewrite (Non_disjoint_union U A x H'0).
+intro H'1; cut (n = n').
+intro E; rewrite E; auto with sets.
+apply cardinal_unicity with A; auto with sets.
+intros H'0 H'1.
+cut (n' = S n).
+intro E; rewrite E; auto with sets.
+apply cardinal_unicity with (Add U A x); auto with sets.
 Qed.
 
-Lemma incl_st_card_lt:
-  (X: (Ensemble U)) (c1: nat) (cardinal U X c1) ->
-  (Y: (Ensemble U)) (c2: nat) (cardinal U Y c2) -> (Strict_Included U X Y) ->
-    (gt c2 c1).
+Lemma incl_st_card_lt :
+ forall (X:Ensemble U) (c1:nat),
+   cardinal U X c1 ->
+   forall (Y:Ensemble U) (c2:nat),
+     cardinal U Y c2 -> Strict_Included U X Y -> c2 > c1.
 Proof.
-Intros X c1 H'; Elim H'.
-Intros Y c2 H'0; Elim H'0; Auto with sets arith.
-Intro H'1.
-Elim (Strict_Included_strict U (Empty_set U)); Auto with sets arith.
-Clear H' c1 X.
-Intros X n H' H'0 x H'1 Y c2 H'2.
-Elim H'2.
-Intro H'3; Elim (not_SIncl_empty U (Add U X x)); Auto with sets arith.
-Clear H'2 c2 Y.
-Intros X0 c2 H'2 H'3 x0 H'4 H'5; Elim (classic (In U X0 x)).
-Intro H'6; Apply gt_n_S.
-Apply H'0 with Y := (Subtract U (Add U X0 x0) x).
-ElimType (pred (S c2)) = c2; Auto with sets arith.
-Apply card_soustr_1; Auto with sets arith.
-Apply incl_st_add_soustr; Auto with sets arith.
-Elim (classic x == x0).
-Intros H'6 H'7; Apply gt_n_S.
-Apply H'0 with Y := X0; Auto with sets arith.
-Apply sincl_add_x with x := x0.
-Rewrite <- H'6; Auto with sets arith.
-Pattern 1 x0; Rewrite <- H'6; Trivial with sets arith.
-Intros H'6 H'7; Red in H'5.
-Elim H'5; Intros H'8 H'9; Try Exact H'8; Clear H'5.
-Red in H'8.
-Generalize (H'8 x).
-Intro H'5; LApply H'5; Auto with sets arith.
-Intro H; Elim Add_inv with U X0 x0 x; Auto with sets arith.
-Intro; Absurd (In U X0 x); Auto with sets arith.
-Intro; Absurd x==x0; Auto with sets arith.
+intros X c1 H'; elim H'.
+intros Y c2 H'0; elim H'0; auto with sets arith.
+intro H'1.
+elim (Strict_Included_strict U (Empty_set U)); auto with sets arith.
+clear H' c1 X.
+intros X n H' H'0 x H'1 Y c2 H'2.
+elim H'2.
+intro H'3; elim (not_SIncl_empty U (Add U X x)); auto with sets arith.
+clear H'2 c2 Y.
+intros X0 c2 H'2 H'3 x0 H'4 H'5; elim (classic (In U X0 x)).
+intro H'6; apply gt_n_S.
+apply H'0 with (Y := Subtract U (Add U X0 x0) x).
+elimtype (pred (S c2) = c2); auto with sets arith.
+apply card_soustr_1; auto with sets arith.
+apply incl_st_add_soustr; auto with sets arith.
+elim (classic (x = x0)).
+intros H'6 H'7; apply gt_n_S.
+apply H'0 with (Y := X0); auto with sets arith.
+apply sincl_add_x with (x := x0).
+rewrite <- H'6; auto with sets arith.
+pattern x0 at 1 in |- *; rewrite <- H'6; trivial with sets arith.
+intros H'6 H'7; red in H'5.
+elim H'5; intros H'8 H'9; try exact H'8; clear H'5.
+red in H'8.
+generalize (H'8 x).
+intro H'5; lapply H'5; auto with sets arith.
+intro H; elim Add_inv with U X0 x0 x; auto with sets arith.
+intro; absurd (In U X0 x); auto with sets arith.
+intro; absurd (x = x0); auto with sets arith.
 Qed.
 
-Lemma incl_card_le:
-  (X,Y: (Ensemble U)) (n,m: nat) (cardinal U X n) -> (cardinal U Y m) -> 
-  (Included U X Y) -> (le n m).
+Lemma incl_card_le :
+ forall (X Y:Ensemble U) (n m:nat),
+   cardinal U X n -> cardinal U Y m -> Included U X Y -> n <= m.
 Proof.
-Intros;
-Elim Included_Strict_Included with U X Y; Auto with sets arith; Intro.
-Cut (gt m n); Auto with sets arith.
-Apply incl_st_card_lt with X := X Y := Y; Auto with sets arith.
-Generalize H0; Rewrite <- H2; Intro.
-Cut n=m.
-Intro E; Rewrite E; Auto with sets arith.
-Apply cardinal_unicity with X; Auto with sets arith.
+intros; elim Included_Strict_Included with U X Y; auto with sets arith; intro.
+cut (m > n); auto with sets arith.
+apply incl_st_card_lt with (X := X) (Y := Y); auto with sets arith.
+generalize H0; rewrite <- H2; intro.
+cut (n = m).
+intro E; rewrite E; auto with sets arith.
+apply cardinal_unicity with X; auto with sets arith.
 Qed.
 
-Lemma G_aux:
-  (P:(Ensemble U) ->Prop)
-  ((X:(Ensemble U))
-   (Finite U X) -> ((Y:(Ensemble U)) (Strict_Included U Y X) ->(P Y)) ->(P X)) ->
-  (P (Empty_set U)).
+Lemma G_aux :
+ forall P:Ensemble U -> Prop,
+   (forall X:Ensemble U,
+      Finite U X ->
+      (forall Y:Ensemble U, Strict_Included U Y X -> P Y) -> P X) ->
+   P (Empty_set U).
 Proof.
-Intros P H'; Try Assumption.
-Apply H'; Auto with sets.
-Clear H'; Auto with sets.
-Intros Y H'; Try Assumption.
-Red in H'.
-Elim H'; Intros H'0 H'1; Try Exact H'1; Clear H'.
-LApply (less_than_empty U Y); [Intro H'3; Try Exact H'3 | Assumption].
-Elim H'1; Auto with sets.
+intros P H'; try assumption.
+apply H'; auto with sets.
+clear H'; auto with sets.
+intros Y H'; try assumption.
+red in H'.
+elim H'; intros H'0 H'1; try exact H'1; clear H'.
+lapply (less_than_empty U Y); [ intro H'3; try exact H'3 | assumption ].
+elim H'1; auto with sets.
 Qed.
 
-Hints Unfold  not.
+Hint Unfold not.
 
-Lemma Generalized_induction_on_finite_sets:
-  (P:(Ensemble U) ->Prop)
-  ((X:(Ensemble U))
-   (Finite U X) -> ((Y:(Ensemble U)) (Strict_Included U Y X) ->(P Y)) ->(P X)) ->
-  (X:(Ensemble U)) (Finite U X) ->(P X).
+Lemma Generalized_induction_on_finite_sets :
+ forall P:Ensemble U -> Prop,
+   (forall X:Ensemble U,
+      Finite U X ->
+      (forall Y:Ensemble U, Strict_Included U Y X -> P Y) -> P X) ->
+   forall X:Ensemble U, Finite U X -> P X.
 Proof.
-Intros P H'0 X H'1.
-Generalize P H'0; Clear H'0 P.
-Elim H'1.
-Intros P H'0.
-Apply G_aux; Auto with sets.
-Clear H'1 X.
-Intros A H' H'0 x H'1 P H'3.
-Cut (Y:(Ensemble U)) (Included U Y (Add U A x)) ->(P Y); Auto with sets.
-Generalize H'1.
-Apply H'0.
-Intros X K H'5 L Y H'6; Apply H'3; Auto with sets.
-Apply Finite_downward_closed with A := (Add U X x); Auto with sets.
-Intros Y0 H'7.
-Elim (Strict_inclusion_is_transitive_with_inclusion U Y0 Y (Add U X x)); Auto with sets.
-Intros H'2 H'4.
-Elim (Included_Add U Y0 X x);
- [Intro H'14 |
-   Intro H'14; Elim H'14; Intros A' E; Elim E; Intros H'15 H'16; Clear E H'14 |
-   Idtac]; Auto with sets.
-Elim (Included_Strict_Included U Y0 X); Auto with sets.
-Intro H'9; Apply H'5 with Y := Y0; Auto with sets.
-Intro H'9; Rewrite H'9.
-Apply H'3; Auto with sets.
-Intros Y1 H'8; Elim H'8.
-Intros H'10 H'11; Apply H'5 with Y := Y1; Auto with sets.
-Elim (Included_Strict_Included U A' X); Auto with sets.
-Intro H'8; Apply H'5 with Y := A'; Auto with sets.
-Rewrite <- H'15; Auto with sets.
-Intro H'8.
-Elim H'7.
-Intros H'9 H'10; Apply H'10 Orelse Elim H'10; Try Assumption.
-Generalize H'6.
-Rewrite <- H'8.
-Rewrite <- H'15; Auto with sets.
+intros P H'0 X H'1.
+generalize P H'0; clear H'0 P.
+elim H'1.
+intros P H'0.
+apply G_aux; auto with sets.
+clear H'1 X.
+intros A H' H'0 x H'1 P H'3.
+cut (forall Y:Ensemble U, Included U Y (Add U A x) -> P Y); auto with sets.
+generalize H'1.
+apply H'0.
+intros X K H'5 L Y H'6; apply H'3; auto with sets.
+apply Finite_downward_closed with (A := Add U X x); auto with sets.
+intros Y0 H'7.
+elim (Strict_inclusion_is_transitive_with_inclusion U Y0 Y (Add U X x));
+ auto with sets.
+intros H'2 H'4.
+elim (Included_Add U Y0 X x);
+ [ intro H'14
+ | intro H'14; elim H'14; intros A' E; elim E; intros H'15 H'16; clear E H'14
+ | idtac ]; auto with sets.
+elim (Included_Strict_Included U Y0 X); auto with sets.
+intro H'9; apply H'5 with (Y := Y0); auto with sets.
+intro H'9; rewrite H'9.
+apply H'3; auto with sets.
+intros Y1 H'8; elim H'8.
+intros H'10 H'11; apply H'5 with (Y := Y1); auto with sets.
+elim (Included_Strict_Included U A' X); auto with sets.
+intro H'8; apply H'5 with (Y := A'); auto with sets.
+rewrite <- H'15; auto with sets.
+intro H'8.
+elim H'7.
+intros H'9 H'10; apply H'10 || elim H'10; try assumption.
+generalize H'6.
+rewrite <- H'8.
+rewrite <- H'15; auto with sets.
 Qed.
 
-End Finite_sets_facts.
+End Finite_sets_facts.
\ No newline at end of file