diff options
Diffstat (limited to 'theories/Wellfounded/Disjoint_Union.v')
| -rw-r--r-- | theories/Wellfounded/Disjoint_Union.v | 16 |
1 files changed, 7 insertions, 9 deletions
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. |