proposition: Lemma acc_union_alt_weak : forall a, (forall b, refl_trans_clos (compose_rel R2 (refl_trans_clos R1)) b a -> Acc R1 b) -> (forall b, refl_trans_clos R1 b a -> Acc (compose_rel (refl_trans_clos R1) R2) b) -> Acc (union _ R1 R2) a.
proof: Proof. intros a H1a H2a. apply acc_union_weak; trivial. clear H1a. apply Acc_intro; intros b4 H. inversion H as [a4 b2 a1 H' H21]; clear H; subst. assert (Acc_b2 := H2a b2 H21). revert a H2a b4 H' H21; induction Acc_b2 as [b2 Acc_b2 IH]. intros a Ha b4 H' H21. apply Acc_intro. intros b6 H. inversion H as [a6 b5 a4 H65 H54]; clear H; subst. apply IH with b5 b4; trivial. apply Comp with b4; trivial. intros b7 H7. apply Acc_b2. apply Comp with b4; trivial. Qed.
imports: Coq(Setoid Relations List Wellfounded)