Remplacement de Induction/Destruct par NewInduction/NewDestruct

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

12 files changed, 105 insertions, 118 deletions

diff --git a/theories/Sets/Constructive_sets.v b/theories/Sets/Constructive_sets.v
index 9d24ae433..78ad3d2f2 100755
--- a/theories/Sets/Constructive_sets.v
+++ b/theories/Sets/Constructive_sets.v
@@ -38,7 +38,7 @@ Qed.
 
 Lemma Noone_in_empty: (x: U) ~ (In U (Empty_set U) x).
 Proof.
-Intro x; Red; Induction 1.
+Red; NewDestruct 1.
 Qed.
 Hints Resolve Noone_in_empty.
 
diff --git a/theories/Sets/Finite_sets.v b/theories/Sets/Finite_sets.v
index 1e0c05450..1e7168791 100755
--- a/theories/Sets/Finite_sets.v
+++ b/theories/Sets/Finite_sets.v
@@ -59,8 +59,8 @@ Lemma cardinal_invert :
    [n:nat] (EXT A | (EXT x | 
            X == (Add U A x) /\ ~ (In U A x) /\ (cardinal U A n))) end.
 Proof.
-Induction 1; Simpl; Auto.
-Intros; Exists A; Exists x; Auto.
+NewInduction 1; Simpl; Auto.
+Exists A; Exists x; Auto.
 Qed.
 
 Lemma cardinal_elim :
diff --git a/theories/Sets/Image.v b/theories/Sets/Image.v
index db41d6ac6..d5f42e3f9 100755
--- a/theories/Sets/Image.v
+++ b/theories/Sets/Image.v
@@ -62,11 +62,11 @@ Split; Red; Intros x0 H'.
 Elim H'; Intros.
 Rewrite H0.
 Elim Add_inv with U X x x1; Auto with sets.
-Induction 1; Auto with sets.
+NewDestruct 1; Auto with sets.
 Elim Add_inv with V (Im X f) (f x) x0; Auto with sets.
-Induction 1; Intros.
-Rewrite H1; Auto with sets.
-Induction 1; Auto with sets.
+NewDestruct 1 as [x0 H y H0].
+Rewrite H0; Auto with sets.
+NewDestruct 1; Auto with sets.
 Qed.
 
 Lemma image_empty: (f: U -> V) (Im (Empty_set U) f) == (Empty_set V).
@@ -110,10 +110,10 @@ Unfold injective; Intros f H.
 Cut (EXT x | ~ ((y: U) (f x) == (f y) -> x == y)).
 2: Apply not_all_ex_not with P:=[x:U](y: U) (f x) == (f y) -> x == y; 
    Trivial with sets.
-Induction 1; Intros x C; Exists x.
+NewDestruct 1 as [x C]; Exists x.
 Cut (EXT y | ~((f x)==(f y)->x==y)).
 2: Apply not_all_ex_not with P:=[y:U](f x)==(f y)->x==y; Trivial with sets.
-Induction 1; Intros y D; Exists y.
+NewDestruct 1 as [y D]; Exists y.
 Apply imply_to_and; Trivial with sets.
 Qed.
 
@@ -140,21 +140,21 @@ Lemma injective_preserves_cardinal:
   (A: (Ensemble U)) (f: U -> V) (n: nat) (injective f) -> (cardinal ? A n) ->
    (n': nat) (cardinal ? (Im A f) n') -> n' = n.
 Proof.
-Induction 2; Auto with sets.
+NewInduction 2 as [|A n H'0 H'1 x H'2]; Auto with sets.
 Rewrite (image_empty f).
 Intros n' CE.
 Apply cardinal_unicity with V (Empty_set V); Auto with sets.
-Intros A0 n0 H'0 H'1 x H'2 n'.
-Rewrite (Im_add A0 x f).
+Intro n'.
+Rewrite (Im_add A x f).
 Intro H'3.
-Elim cardinal_Im_intro with A0 f n0; Trivial with sets.
+Elim cardinal_Im_intro with A f n; Trivial with sets.
 Intros i CI.
 LApply (H'1 i); Trivial with sets.
-Cut ~ (In ? (Im A0 f) (f x)).
-Intros.
-Apply cardinal_unicity with V (Add ? (Im A0 f) (f x)); Trivial with sets.
+Cut ~ (In ? (Im A f) (f x)).
+Intros H0 H1.
+Apply cardinal_unicity with V (Add ? (Im A f) (f x)); Trivial with sets.
 Apply card_add; Auto with sets.
-Rewrite <- H2; Trivial with sets.
+Rewrite <- H1; Trivial with sets.
 Red; Intro; Apply H'2.
 Apply In_Image_elim with f; Trivial with sets.
 Qed.
@@ -163,17 +163,17 @@ Lemma cardinal_decreases:
   (A: (Ensemble U)) (f: U -> V) (n: nat) (cardinal U A n) ->
    (n': nat) (cardinal V (Im A f) n') -> (le n' n).
 Proof.
-Induction 1; Auto with sets.
+NewInduction 1 as [|A n H'0 H'1 x H'2]; Auto with sets.
 Rewrite (image_empty f); Intros.
 Cut n' = O.
 Intro E; Rewrite E; Trivial with sets.
 Apply cardinal_unicity with V (Empty_set V); Auto with sets.
-Intros A0 n0 H'0 H'1 x H'2 n'.
-Rewrite (Im_add A0 x f).
-Elim cardinal_Im_intro with A0 f n0; Trivial with sets.
+Intro n'.
+Rewrite (Im_add A x f).
+Elim cardinal_Im_intro with A f n; Trivial with sets.
 Intros p C H'3.
 Apply le_trans with (S p).
-Apply card_Add_gen with V (Im A0 f) (f x); Trivial with sets.
+Apply card_Add_gen with V (Im A f) (f x); Trivial with sets.
 Apply le_n_S; Auto with sets.
 Qed.
 
diff --git a/theories/Sets/Multiset.v b/theories/Sets/Multiset.v
index 68d3ec7a5..37fb47e27 100755
--- a/theories/Sets/Multiset.v
+++ b/theories/Sets/Multiset.v
@@ -42,21 +42,21 @@ Hints Unfold  meq multiplicity.
 
 Lemma meq_refl : (x:multiset)(meq x x).
 Proof.
-Induction x; Auto.
+NewDestruct x; Auto.
 Qed.
 Hints Resolve meq_refl.
 
 Lemma meq_trans : (x,y,z:multiset)(meq x y)->(meq y z)->(meq x z).
 Proof.
 Unfold meq.
-Induction x; Induction y; Induction z.
+NewDestruct x; NewDestruct y; NewDestruct z.
 Intros; Rewrite H; Auto.
 Qed.
 
 Lemma meq_sym : (x,y:multiset)(meq x y)->(meq y x).
 Proof.
 Unfold meq.
-Induction x; Induction y; Auto.
+NewDestruct x; NewDestruct y; Auto.
 Qed.
 Hints Immediate meq_sym.
 
@@ -83,7 +83,7 @@ Require Plus. (* comm. and ass. of plus *)
 Lemma munion_comm : (x,y:multiset)(meq (munion x y) (munion y x)).
 Proof.
 Unfold meq; Unfold multiplicity; Unfold munion.
-Induction x; Induction y; Auto with arith.
+NewDestruct x; NewDestruct y; Auto with arith.
 Qed.
 Hints Resolve munion_comm.
 
@@ -91,14 +91,14 @@ Lemma munion_ass :
       (x,y,z:multiset)(meq (munion (munion x y) z) (munion x (munion y z))).
 Proof.
 Unfold meq; Unfold munion; Unfold multiplicity.
-Induction x; Induction y; Induction z; Auto with arith.
+NewDestruct x; NewDestruct y; NewDestruct z; Auto with arith.
 Qed.
 Hints Resolve munion_ass.
 
 Lemma meq_left :  (x,y,z:multiset)(meq x y)->(meq (munion x z) (munion y z)).
 Proof.
 Unfold meq; Unfold munion; Unfold multiplicity.
-Induction x; Induction y; Induction z.
+NewDestruct x; NewDestruct y; NewDestruct z.
 Intros; Elim H; Auto with arith.
 Qed.
 Hints Resolve meq_left.
@@ -106,7 +106,7 @@ Hints Resolve meq_left.
 Lemma meq_right : (x,y,z:multiset)(meq x y)->(meq (munion z x) (munion z y)).
 Proof.
 Unfold meq; Unfold munion; Unfold multiplicity.
-Induction x; Induction y; Induction z.
+NewDestruct x; NewDestruct y; NewDestruct z.
 Intros; Elim H; Auto.
 Qed.
 Hints Resolve meq_right.
diff --git a/theories/Sets/Uniset.v b/theories/Sets/Uniset.v
index 17b10ae3a..5b28d6c2b 100644
--- a/theories/Sets/Uniset.v
+++ b/theories/Sets/Uniset.v
@@ -54,7 +54,7 @@ Hints Unfold seq.
 
 Lemma leb_refl : (b:bool)(leb b b).
 Proof.
-Induction b; Simpl; Auto.
+NewDestruct b; Simpl; Auto.
 Qed.
 Hints Resolve leb_refl.
 
@@ -70,21 +70,21 @@ Qed.
 
 Lemma seq_refl : (x:uniset)(seq x x).
 Proof.
-Induction x; Unfold seq; Auto.
+NewDestruct x; Unfold seq; Auto.
 Qed.
 Hints Resolve seq_refl.
 
 Lemma seq_trans : (x,y,z:uniset)(seq x y)->(seq y z)->(seq x z).
 Proof.
 Unfold seq.
-Induction x; Induction y; Induction z; Simpl; Intros.
+NewDestruct x; NewDestruct y; NewDestruct z; Simpl; Intros.
 Rewrite H; Auto.
 Qed.
 
 Lemma seq_sym : (x,y:uniset)(seq x y)->(seq y x).
 Proof.
 Unfold seq.
-Induction x; Induction y; Simpl; Auto.
+NewDestruct x; NewDestruct y; Simpl; Auto.
 Qed.
 
 (** uniset union *)
@@ -109,7 +109,7 @@ Hints Resolve union_empty_right.
 Lemma union_comm : (x,y:uniset)(seq (union x y) (union y x)).
 Proof.
 Unfold seq; Unfold charac; Unfold union.
-Induction x; Induction y; Auto with bool.
+NewDestruct x; NewDestruct y; Auto with bool.
 Qed.
 Hints Resolve union_comm.
 
@@ -117,14 +117,14 @@ Lemma union_ass :
       (x,y,z:uniset)(seq (union (union x y) z) (union x (union y z))).
 Proof.
 Unfold seq; Unfold union; Unfold charac.
-Induction x; Induction y; Induction z; Auto with bool.
+NewDestruct x; NewDestruct y; NewDestruct z; Auto with bool.
 Qed.
 Hints Resolve union_ass.
 
 Lemma seq_left :  (x,y,z:uniset)(seq x y)->(seq (union x z) (union y z)).
 Proof.
 Unfold seq; Unfold union; Unfold charac.
-Induction x; Induction y; Induction z.
+NewDestruct x; NewDestruct y; NewDestruct z.
 Intros; Elim H; Auto.
 Qed.
 Hints Resolve seq_left.
@@ -132,7 +132,7 @@ Hints Resolve seq_left.
 Lemma seq_right : (x,y,z:uniset)(seq x y)->(seq (union z x) (union z y)).
 Proof.
 Unfold seq; Unfold union; Unfold charac.
-Induction x; Induction y; Induction z.
+NewDestruct x; NewDestruct y; NewDestruct z.
 Intros; Elim H; Auto.
 Qed.
 Hints Resolve seq_right.
diff --git a/theories/Wellfounded/Disjoint_Union.v b/theories/Wellfounded/Disjoint_Union.v
index 6e9cbf062..44c2f8661 100644
--- a/theories/Wellfounded/Disjoint_Union.v
+++ b/theories/Wellfounded/Disjoint_Union.v
@@ -23,8 +23,8 @@ Notation Le_AsB := (le_AsB A B leA leB).
 
 Lemma acc_A_sum: (x:A)(Acc A leA x)->(Acc A+B Le_AsB (inl A B x)).
 Proof.
- Induction 1;Intros.
- Apply Acc_intro;Intros.
+ NewInduction 1.
+ Apply Acc_intro;Intros y H2.
  Inversion_clear H2.
  Auto with sets.
 Qed.
@@ -32,8 +32,8 @@ Qed.
 Lemma acc_B_sum: (well_founded A leA) ->(x:B)(Acc B leB x)
                         ->(Acc A+B Le_AsB (inr A B x)).
 Proof.
- Induction 2;Intros.
- Apply Acc_intro;Intros.
+ NewInduction 2.
+ Apply Acc_intro;Intros y H3.
  Inversion_clear H3;Auto with sets.
  Apply acc_A_sum;Auto with sets.
 Qed.
@@ -45,12 +45,10 @@ Lemma wf_disjoint_sum:
 Proof.
  Intros.
  Unfold well_founded .
- Induction a.
- Intro a0.
- Apply (acc_A_sum a0).
- Apply (H a0).
+ NewDestruct a as [a|b].
+ Apply (acc_A_sum a).
+ Apply (H a).
 
- Intro b.
  Apply (acc_B_sum H b).
  Apply (H0 b).
 Qed.
diff --git a/theories/Wellfounded/Inclusion.v b/theories/Wellfounded/Inclusion.v
index d2658e717..2038b34bf 100644
--- a/theories/Wellfounded/Inclusion.v
+++ b/theories/Wellfounded/Inclusion.v
@@ -18,7 +18,7 @@ Section WfInclusion.
 
   Lemma Acc_incl: (inclusion A R1 R2)->(z:A)(Acc A R2 z)->(Acc A R1 z).
   Proof.
-    Induction 2;Intros.
+    NewInduction 2.
     Apply Acc_intro;Auto with sets.
   Qed.
 
diff --git a/theories/Wellfounded/Inverse_Image.v b/theories/Wellfounded/Inverse_Image.v
index 9afffc95c..ac828ac1a 100644
--- a/theories/Wellfounded/Inverse_Image.v
+++ b/theories/Wellfounded/Inverse_Image.v
@@ -19,10 +19,10 @@ Section Inverse_Image.
   Local Rof : A->A->Prop := [x,y:A](R (f x) (f y)).
 
   Remark Acc_lemma : (y:B)(Acc B R y)->(x:A)(y=(f x))->(Acc A Rof x).
-    Induction 1; Intros.
-    Apply Acc_intro; Intros.
-    Apply (H1 (f y0)); Try Trivial.
-    Rewrite H2; Trivial.
+    NewInduction 1 as [y _ IHAcc]; Intros x H.
+    Apply Acc_intro; Intros y0 H1.
+    Apply (IHAcc (f y0)); Try Trivial.
+    Rewrite H; Trivial.
   Qed.
 
   Lemma Acc_inverse_image : (x:A)(Acc B R (f x)) -> (Acc A Rof x).
@@ -39,10 +39,10 @@ Section Inverse_Image.
 
 Lemma Acc_inverse_rel :
    (b:B)(Acc B R b)->(x:A)(F x b)->(Acc A RoF x).
-Induction 1; Intros.
-Constructor; Intros.
-Case H3; Intros.
-Apply (H1 x1); Auto.
+NewInduction 1 as [x _ IHAcc]; Intros x0 H2.
+Constructor; Intros y H3.
+NewDestruct H3.
+Apply (IHAcc x1); Auto.
 Save.
 
 
diff --git a/theories/Wellfounded/Lexicographic_Product.v b/theories/Wellfounded/Lexicographic_Product.v
index 39b00e676..b8f74c9ff 100644
--- a/theories/Wellfounded/Lexicographic_Product.v
+++ b/theories/Wellfounded/Lexicographic_Product.v
@@ -8,7 +8,7 @@
 
 (*i $Id$ i*)
 
-(** Authors: Bruno Barras,Cristina Cornes *)
+(** Authors: Bruno Barras, Cristina Cornes *)
 
 Require Eqdep.
 Require Relation_Operators.
@@ -32,14 +32,13 @@ Lemma acc_A_B_lexprod : (x:A)(Acc A leA x)
                 ->(y:(B x))(Acc (B x) (leB x) y)
                         ->(Acc (sigS A B) LexProd (existS A B x y)).
 Proof.
- Induction 1; Intros x0 H0 H1 H2 y.
- Induction 1;Intros.
+ NewInduction 1 as [x _ IHAcc]; Intros H2 y.
+ NewInduction 1 as [x0 H IHAcc0];Intros.
  Apply Acc_intro.
- Induction y0.
- Intros x2 y1 H6.
- Simple Inversion H6;Intros.
- Cut (leA x2 x0);Intros.
- Apply H1;Auto with sets.
+ NewDestruct y as [x2 y1]; Intro H6.
+ Simple Inversion H6; Intro.
+ Cut (leA x2 x);Intros.
+ Apply IHAcc;Auto with sets.
  Intros.
  Apply H2.
  Apply t_trans with x2 ;Auto with sets.
@@ -48,20 +47,16 @@ Proof.
  Apply H2.
  Auto with sets.
 
- Injection H8.
- Induction 2.
- Injection H9.
- Induction 2;Auto with sets.
+ Injection H1.
+ NewDestruct 2.
+ Injection H3.
+ NewDestruct 2;Auto with sets.
 
- Elim H8.
- Generalize y2 y' H9 H7 .
- Replace x3 with x0.
- Clear  H7 H8 H9 y2 y' x3 H6 y1 x2 y0.
- Intros.
- Apply H5.
- Elim inj_pair2 with A B x0 y' x1 ;Auto with sets.
-
- Injection H9;Auto with sets.
+ Rewrite <- H1.
+ Injection H3; Intros _ Hx1.
+ Subst x1.
+ Apply IHAcc0.
+ Elim inj_pair2 with A B x y' x0; Assumption.
 Qed.
 
 Theorem wf_lexprod: 
@@ -69,7 +64,7 @@ Theorem wf_lexprod:
              -> (well_founded (sigS A B) LexProd).
 Proof.
  Intros wfA wfB;Unfold well_founded .
- Induction a;Intros.
+ NewDestruct a.
  Apply acc_A_B_lexprod;Auto with sets;Intros.
  Red in wfB.
  Auto with sets.
@@ -108,13 +103,13 @@ i*)
 
   Lemma Acc_symprod: (x:A)(Acc A leA x)->(y:B)(Acc B leB y)
                         ->(Acc (A*B) Symprod (x,y)).
-Proof.
- Induction 1;Intros.
- Elim H2;Intros.
- Apply Acc_intro;Intros.
+ Proof.
+ NewInduction 1 as [x _ IHAcc]; Intros y H2.
+ NewInduction H2 as [x1 H3 IHAcc1].
+ Apply Acc_intro;Intros y H5.
  Inversion_clear H5;Auto with sets.
- Apply H1;Auto with sets.
- Apply Acc_intro;Auto with sets.
+ Apply IHAcc; Auto.
+ Apply Acc_intro;Trivial.
 Qed.
 
 
@@ -122,7 +117,7 @@ Lemma wf_symprod: (well_founded A leA)->(well_founded B leB)
                         ->(well_founded (A*B) Symprod).
 Proof.
  Red.
- Induction a;Intros.
+ NewDestruct a.
  Apply Acc_symprod;Auto with sets.
 Qed.
 
@@ -161,24 +156,24 @@ Qed.
   Lemma Acc_swapprod: (x,y:A)(Acc A R x)->(Acc A R y)
                                 ->(Acc A*A SwapProd (x,y)).
 Proof.
- Induction 1;Intros.
+ NewInduction 1 as [x0 _ IHAcc0];Intros H2.
  Cut (y0:A)(R y0 x0)->(Acc ? SwapProd (y0,y)).
- Clear  H1.
- Elim H2;Intros.
+ Clear  IHAcc0.
+ NewInduction H2 as [x1 _ IHAcc1]; Intros H4.
  Cut (y:A)(R y x1)->(Acc ? SwapProd (x0,y)).
- Clear  H3.
+ Clear  IHAcc1.
  Intro.
  Apply Acc_intro.
- Induction y0;Intros.
+ NewDestruct y; Intro H5.
  Inversion_clear H5.
- Inversion_clear H6;Auto with sets.
+ Inversion_clear H0;Auto with sets.
 
  Apply swap_Acc.
- Inversion_clear H6;Auto with sets.
+ Inversion_clear H0;Auto with sets.
 
  Intros.
- Apply H3;Auto with sets;Intros.
- Apply Acc_inv with (y1,x1) ;Auto with sets.
+ Apply IHAcc1;Auto with sets;Intros.
+ Apply Acc_inv with (y0,x1) ;Auto with sets.
  Apply sp_noswap.
  Apply right_sym;Auto with sets.
 
@@ -189,7 +184,7 @@ Qed.
   Lemma wf_swapprod: (well_founded A R)->(well_founded A*A SwapProd).
 Proof.
  Red.
- Induction a;Intros.
+ NewDestruct a;Intros.
  Apply Acc_swapprod;Auto with sets.
 Qed.
 
diff --git a/theories/Wellfounded/Transitive_Closure.v b/theories/Wellfounded/Transitive_Closure.v
index 1198c1d47..c650d4675 100644
--- a/theories/Wellfounded/Transitive_Closure.v
+++ b/theories/Wellfounded/Transitive_Closure.v
@@ -24,23 +24,19 @@ Section Wf_Transitive_Closure.
   Qed.
 
   Lemma Acc_clos_trans: (x:A)(Acc A R x)->(Acc A trans_clos x).
-    Induction 1.
-    Intros x0 H0 H1.
+    NewInduction 1 as [x0 _ H1].
     Apply Acc_intro.
     Intros y H2.
-    Generalize H1 .
-    Elim H2;Auto with sets.
-    Intros x1 y0 z H3 H4 H5 H6 H7.
-    Apply Acc_inv with y0 ;Auto with sets.
+    NewInduction H2;Auto with sets.
+    Apply Acc_inv with y ;Auto with sets.
   Qed.
 
   Hints Resolve Acc_clos_trans.
 
   Lemma Acc_inv_trans: (x,y:A)(trans_clos y x)->(Acc A R x)->(Acc A R y).
   Proof.
-    Induction 1;Auto with sets.
-    Intros x0 y0 H0 H1.
-    Apply Acc_inv with y0 ;Auto with sets.
+    NewInduction 1 as [|x y];Auto with sets.
+    Intro; Apply Acc_inv with y; Assumption.
   Qed.
 
   Theorem wf_clos_trans: (well_founded A R)  ->(well_founded A trans_clos).
diff --git a/theories/Wellfounded/Union.v b/theories/Wellfounded/Union.v
index 084538d8c..ee45a9476 100644
--- a/theories/Wellfounded/Union.v
+++ b/theories/Wellfounded/Union.v
@@ -26,35 +26,34 @@ Remark strip_commut:
       (commut A R1 R2)->(x,y:A)(clos_trans A R1 y x)->(z:A)(R2 z y)
             ->(EX y':A | (R2 y' x) & (clos_trans A R1 z y')).
 Proof.
- Induction 2;Intros.
- Elim H with y0 x0 z ;Auto with sets;Intros.
- Exists x1;Auto with sets.
+ NewInduction 2 as [x y|x y z H0 IH1 H1 IH2]; Intros.
+ Elim H with y x z ;Auto with sets;Intros x0 H2 H3.
+ Exists x0;Auto with sets.
 
- Elim H2 with z0 ;Auto with sets;Intros.
- Elim H4 with x1 ;Auto with sets;Intros.
- Exists x2;Auto with sets.
- Apply t_trans with x1 ;Auto with sets.
+ Elim IH1 with z0 ;Auto with sets;Intros.
+ Elim IH2 with x0 ;Auto with sets;Intros.
+ Exists x1;Auto with sets.
+ Apply t_trans with x0; Auto with sets.
 Qed.
 
 
   Lemma Acc_union:  (commut A R1 R2)->((x:A)(Acc A R2 x)->(Acc A R1 x))
                          ->(a:A)(Acc A R2 a)->(Acc A Union a).
 Proof.
- Induction 3.
- Intros.
+ NewInduction 3 as [x H1 H2].
  Apply Acc_intro;Intros.
- Elim H4;Intros;Auto with sets.
+ Elim H3;Intros;Auto with sets.
  Cut (clos_trans A  R1 y x);Auto with sets.
  ElimType (Acc A (clos_trans A R1) y);Intros.
  Apply Acc_intro;Intros.
- Elim H9;Intros.
- Apply H7;Auto with sets.
+ Elim H8;Intros.
+ Apply H6;Auto with sets.
  Apply t_trans with x0 ;Auto with sets.
 
  Elim strip_commut with x x0 y0 ;Auto with sets;Intros.
  Apply Acc_inv_trans with x1 ;Auto with sets.
  Unfold union .
- Elim H12;Auto with sets;Intros.
+ Elim H11;Auto with sets;Intros.
  Apply t_trans with y1 ;Auto with sets.
 
  Apply (Acc_clos_trans A).
diff --git a/theories/Wellfounded/Well_Ordering.v b/theories/Wellfounded/Well_Ordering.v
index ebd4925d1..49595dd2b 100644
--- a/theories/Wellfounded/Well_Ordering.v
+++ b/theories/Wellfounded/Well_Ordering.v
@@ -65,8 +65,7 @@ Proof.
  Intros.
  Apply (sup A B x).
  Unfold 1 B .
- Induction 1.
- Intros.
+ NewDestruct 1 as [x0].
  Apply (H1 x0);Auto.
 Qed.