proposition: Lemma reg_dp : forall (R1 : relation term), (forall s t, R1 s t -> forall x, In x (var_list s) -> In x (var_list t)) -> forall s t, dp R1 s t -> forall x, In x (var_list s) -> In x (var_list t).
proof: Proof. intros R1 R1_reg v u H. inversion H as [u' r p g k r_R_u Sub Dg H2 H3]; clear H; subst. intros x x_in_k; apply R1_reg with r; trivial. refine (var_in_subterm _ _ _ Sub x_in_k). Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec) CoLoR(NatCompat)