proposition: Lemma acc_union_alt : well_founded R1 -> forall a, (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 W1'; split. intro Ha; apply acc_union_weak; trivial. apply Acc_intro; intros b4 H. inversion H as [a4 b2 a1 H' H21]; clear H; subst. assert (Acc_b2 := Ha b2 H21). revert a Ha 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. intros Acc_a b H; apply Acc_incl with (trans_clos (union _ R1 R2)). clear b H; 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. inversion H as [a' | b' a' K]; clear H. apply acc_trans; assumption. subst; apply Acc_inv with a. apply acc_trans; assumption. apply trans_incl with R1; trivial. intros x y H; left; assumption. Qed.
imports: Coq(Setoid Relations List Wellfounded)