diff options
Diffstat (limited to 'theories/Wellfounded/Disjoint_Union.v')
-rw-r--r-- | theories/Wellfounded/Disjoint_Union.v | 74 |
1 files changed, 37 insertions, 37 deletions
diff --git a/theories/Wellfounded/Disjoint_Union.v b/theories/Wellfounded/Disjoint_Union.v index 940569bd..1e22730b 100644 --- a/theories/Wellfounded/Disjoint_Union.v +++ b/theories/Wellfounded/Disjoint_Union.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Disjoint_Union.v 5920 2004-07-16 20:01:26Z herbelin $ i*) +(*i $Id: Disjoint_Union.v 9245 2006-10-17 12:53:34Z notin $ i*) (** Author: Cristina Cornes From : Constructing Recursion Operators in Type Theory @@ -15,41 +15,41 @@ Require Import Relation_Operators. Section Wf_Disjoint_Union. -Variables A B : Set. -Variable leA : A -> A -> Prop. -Variable leB : B -> B -> Prop. - -Notation Le_AsB := (le_AsB A B leA leB). - -Lemma acc_A_sum : forall x:A, Acc leA x -> Acc Le_AsB (inl B x). -Proof. - induction 1. - apply Acc_intro; intros y H2. - inversion_clear H2. - auto with sets. -Qed. - -Lemma acc_B_sum : - well_founded leA -> forall x:B, Acc leB x -> Acc Le_AsB (inr A x). -Proof. - induction 2. - apply Acc_intro; intros y H3. - inversion_clear H3; auto with sets. - apply acc_A_sum; auto with sets. -Qed. - - -Lemma wf_disjoint_sum : - well_founded leA -> well_founded leB -> well_founded Le_AsB. -Proof. - intros. - unfold well_founded in |- *. - destruct a as [a| b]. - apply (acc_A_sum a). - apply (H a). - - apply (acc_B_sum H b). - apply (H0 b). -Qed. + Variables A B : Set. + Variable leA : A -> A -> Prop. + Variable leB : B -> B -> Prop. + + Notation Le_AsB := (le_AsB A B leA leB). + + Lemma acc_A_sum : forall x:A, Acc leA x -> Acc Le_AsB (inl B x). + Proof. + induction 1. + apply Acc_intro; intros y H2. + inversion_clear H2. + auto with sets. + Qed. + + Lemma acc_B_sum : + well_founded leA -> forall x:B, Acc leB x -> Acc Le_AsB (inr A x). + Proof. + induction 2. + apply Acc_intro; intros y H3. + inversion_clear H3; auto with sets. + apply acc_A_sum; auto with sets. + Qed. + + + Lemma wf_disjoint_sum : + well_founded leA -> well_founded leB -> well_founded Le_AsB. + Proof. + intros. + unfold well_founded in |- *. + destruct a as [a| b]. + apply (acc_A_sum a). + apply (H a). + + apply (acc_B_sum H b). + apply (H0 b). + Qed. End Wf_Disjoint_Union.
\ No newline at end of file |