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