aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2003-09-23 21:00:49 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2003-09-23 21:00:49 +0000
commit19dd83cf1b0e57fb13a8d970251822afd6a04ced (patch)
tree7f5630f3f9a54d06f48ad5a1da6d2987332cc01b
parent8a95a21a90188d8ef4bd790563a63fdf9b4318a9 (diff)
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
-rwxr-xr-xtheories/Sets/Constructive_sets.v2
-rwxr-xr-xtheories/Sets/Finite_sets.v4
-rwxr-xr-xtheories/Sets/Image.v38
-rwxr-xr-xtheories/Sets/Multiset.v14
-rw-r--r--theories/Sets/Uniset.v16
-rw-r--r--theories/Wellfounded/Disjoint_Union.v16
-rw-r--r--theories/Wellfounded/Inclusion.v2
-rw-r--r--theories/Wellfounded/Inverse_Image.v16
-rw-r--r--theories/Wellfounded/Lexicographic_Product.v73
-rw-r--r--theories/Wellfounded/Transitive_Closure.v14
-rw-r--r--theories/Wellfounded/Union.v25
-rw-r--r--theories/Wellfounded/Well_Ordering.v3
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.