proposition: Lemma wf_Rcdp_rest : well_founded (Rcdp_rest dps).
proof: Proof. apply wf_incl with (sdp.Rcdp R_rules dps); [ intros x y [H H0]; assumption | apply wf_Rcdp ]. Qed.
imports: Coq(Setoid List Relations Wellfounded PeanoNat) CoLoR(weaved_relation list_permut terminaison)