proposition: Lemma one_step_subterm_acc_rdp_acc_rdp : forall R1 R2 f l1 l2, one_step_list (one_step R1) l2 l1 -> Acc (rdp_step R2 R1) (Term f l1) -> Acc (rdp_step R2 R1) (Term f l2).
proof: Proof. intros R1 R2 f l1 l2 H Acc_t1; apply Acc_intro; intros t H'. apply Acc_inv with (Term f l1); trivial. apply one_step_subterm_rdp_rdp with l2; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec) CoLoR(NatCompat)