proposition: Lemma acc_R_acc_dp : forall t, Acc (one_step R) t -> Acc Rcdp t.
proof: Proof. intros t Acc_t. apply Acc_incl with (rdp_step (axiom (ddp R)) R). intros t1 t2 K; inversion K; clear K; subst. apply Rdp_step with l2; trivial. inversion H0; clear H0; subst; apply instance; apply cdp_in_dpR; trivial. apply acc_one_step_acc_ddp; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term_spec equational_theory_spec dp) CoLoR(NatCompat)