proposition: Lemma wf_R : well_founded (Eqt.one_step R_rules).
proof: Proof. apply wf_incl with Tlt; [| assumption ]; intros x y H; apply stable_monotone_R_term with R_rules; assumption. Qed.
imports: Coq(Setoid List Relations Wellfounded PeanoNat) CoLoR(weaved_relation list_permut terminaison)