proposition: Lemma ddp_necessary : forall R, (forall x t, ~ (R t (Var x))) -> well_founded (one_step R) -> well_founded (ddp_step R).
proof: Proof. intros R HR Wf. intro t; apply acc_one_step_acc_ddp; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec) CoLoR(NatCompat)