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