proposition: Lemma rwr_subterm_rdp_rdp : forall R1 R2 f l1 l2 t, refl_trans_clos (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'. inversion H' as [f' l2' l3 t' K K']; clear H'; subst. apply Rdp_step with l3; trivial. apply refl_trans_clos_is_trans with l2; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec) CoLoR(NatCompat)