proposition: Lemma wf_Rcdp : well_founded (sdp.Rcdp R_rules dps).
proof: Proof. apply wf_incl with Tlt; [| assumption ]; intros x y H; inversion H; inversion H1; subst; apply rtc_R_step with l2; [| assumption ]; rewrite <- H4; apply dps_strictly_decrease; assumption. Qed.
imports: Coq(Setoid List Relations Wellfounded PeanoNat) CoLoR(weaved_relation list_permut terminaison)