proposition: Lemma acc_union : well_founded R1 -> forall a, Acc (compose_rel R2 (refl_trans_clos R1)) a <-> Acc (union _ R1 R2) a.
proof: Proof. intros W1'. assert (W1 := wf_trans W1'); clear W1'. intros a; split. intro Acc_a; 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'. revert IH2 Acc_a. pattern a; apply (well_founded_ind W1); clear a. intros a IH1 IH2 Acc_a. apply Acc_intro. intros b [H1 | H2]. apply IH1. apply t_step; 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. apply Acc_intro; intros c H2. apply Acc_inv with a; trivial. 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. apply IH2. apply Comp with a; trivial. apply r_step. intro Acc_a; apply Acc_incl with (trans_clos (union _ R1 R2)). intros a1 a3 H; inversion H as [b1 b2 b3 H1 H2]; clear H; subst a1 a3. inversion H2 as [b | a2 a3 K2]; clear H2; subst. left; right; assumption. apply t_trans with b2. right; assumption. apply trans_incl with R1; trivial. intros x y H; left; assumption. apply acc_trans; assumption. Qed.
imports: Coq(Setoid Relations List Wellfounded)