proposition: Lemma acc_union_rest : forall A (R1 R2 : relation A) (P : A -> Prop), (forall (a b : A), P a -> R1 b a -> P b) -> (forall (a b : A), P a -> R2 b a -> P b) -> (forall a, P a -> Acc R1 a) -> forall a, P a -> Acc (compose_rel R2 (refl_trans_clos R1)) a -> Acc (union _ R1 R2) a.
proof: Proof. intros A R1 R2 P Inv1 Inv2 W1' a Wa Acc_a. rewrite wf_rest in W1'. set (R1' := fun a b => R1 a b /\ P a /\ P b) in *. assert (W1 := wf_trans W1'); clear W1'. revert Wa; 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 Wa. apply Acc_intro. intros b [H1 | H2]. apply IH1. apply t_step; repeat split; trivial. apply Inv1 with a; 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 Inv1 with a; trivial. apply IH2. apply Comp with a; trivial. apply r_step. apply Inv2 with a; trivial. trivial. Qed.
imports: Coq(Setoid Relations List Wellfounded)