proposition: Lemma wf_union_alt : well_founded R1 -> (well_founded (compose_rel (refl_trans_clos R1) R2) <-> well_founded (union _ R1 R2)).
proof: Proof. intros W1'; split. intro W; intro a; rewrite <- acc_union; trivial. assert (W1 := wf_trans W1'); clear W1'. apply Acc_intro. intros b4 H. inversion H as [a4 b2 a1 H' H21]; clear H; subst. clear a H21. revert b4 H'. pattern b2; apply (well_founded_ind (wf_trans W)); clear b2. intros a IH b H. apply Acc_intro; intros c K. inversion K as [d' c' b' H1 H2];clear K; subst. apply IH with c'; trivial. left; apply Comp with b; trivial. intros W 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 H1 as [b | a2 a3 K1]; clear H1; subst. left; right; assumption. apply trans_clos_is_trans with b2. apply trans_incl with R1; trivial. intros x y H; left; assumption. left; right; assumption. apply acc_trans; apply W. Qed.
imports: Coq(Setoid Relations List Wellfounded)