proposition: Lemma acc_comp_incl : forall R, (forall a, Acc R a -> Acc (union _ R1 R2) a) -> forall a, Acc R a -> Acc (compose_rel (refl_trans_clos R1) R2) a.
proof: Proof. intros R H a Acc_a. apply Acc_incl with (trans_clos (union _ R1 R2)). clear; intros a b H. inversion H as [c1 c2 c3 K1 K2]; clear H; subst. inversion K1 as [c | b1 b2 K3 K4]; clear K1; subst. left; right; assumption. apply trans_clos_is_trans with c2. apply trans_incl with R1; trivial. clear; intros a b H; left; assumption. left; right; assumption. apply acc_trans. apply H; assumption. Qed.
imports: Coq(Setoid Relations List Wellfounded)