proposition: Lemma acc_one_step_acc_ddp : forall R, (forall x t, ~ (R t (Var x))) -> forall t, Acc (one_step R) t -> Acc (ddp_step R) t.
proof: Proof. intros R HR t Acc_t. apply Acc_incl with (dp_step R). clear t Acc_t; intros t1 t2 H; inversion H; clear H; subst. apply Rdp_step with l2; trivial. inversion H1; clear H1; subst; apply instance. apply ddp_is_dp; assumption. apply acc_one_step_acc_dp; assumption. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec) CoLoR(NatCompat)