proposition: Lemma acc_union_weak : forall a, Acc (compose_rel R2 (refl_trans_clos R1)) a -> (forall b, refl_trans_clos (compose_rel R2 (refl_trans_clos R1)) b a -> Acc R1 b) -> Acc (union _ R1 R2) a.
proof: Proof. intros a Acc_a H; induction Acc_a as [a Acc_a' IH2]. assert (Acc_a : Acc (compose_rel R2 (refl_trans_clos R1)) a). apply Acc_intro; trivial. clear Acc_a'. assert (Acc1_a : Acc R1 a). apply H; left. revert IH2 H Acc_a. induction Acc1_a as [a Acc1_a IH1]. intros IH2 H Acc_a. apply Acc_intro. intros b [H1 | H2]. apply IH1; trivial. intros c H2; apply IH2. inversion H2 as [c' d' b' h H']; subst. apply Comp with d'; trivial. apply refl_trans_clos_is_trans with b; trivial. right; left; trivial. intros c K; inversion K; clear K; subst. apply Acc1_a; assumption. apply H. rewrite trans_clos_trans_clos_alt in H0. inversion H0; clear H0; subst. right; left. inversion H2; clear H2; subst. apply Comp with a2; trivial. apply refl_trans_clos_is_trans with b; trivial. right; left; exact H1. inversion H3; clear H3; subst. apply refl_trans_clos_is_trans with y; trivial. right; rewrite trans_clos_trans_clos_alt; assumption. right; left. apply Comp with a2; trivial. apply refl_trans_clos_is_trans with b; trivial. right; left; exact H1. apply Acc_intro; intros c K. apply Acc_inv with a; trivial. inversion K; clear K; subst. apply Comp with a2; trivial. apply refl_trans_clos_is_trans with b; trivial. right; left; exact H1. apply IH2. apply Comp with a; [assumption | left]. intros c K; apply H. apply refl_trans_clos_is_trans with b; trivial. right; left; apply Comp with a; [assumption | left]. Qed.
imports: Coq(Setoid Relations List Wellfounded)