proposition: Lemma rwr_list_incl : forall (R1 R2 : term -> term -> Prop), (forall t1 t2, R1 t1 t2 -> R2 t1 t2) -> forall l1 l2, rwr_list (one_step R1) l1 l2 -> rwr_list (one_step R2) l1 l2.
proof: Proof. intros R1 R2 Incl. apply trans_incl. do 2 intro; apply one_step_list_incl. do 2 intro; apply one_step_incl; assumption. Qed.
imports: Coq(List Relations Wellfounded Arith Setoid) CoLoR(closure more_list weaved_relation dickson term_spec equational_theory_spec)