proposition: Lemma rtc_R_step : forall t f l1 l2, Tlt t (M.Term f l1) -> refl_trans_clos (one_step_list (Eqt.one_step R_rules)) l1 l2 -> Tlt t (M.Term f l2).
proof: Proof. intros t f l1 l H H0; destruct H0; [ assumption |]; induction H0; [| apply IHtrans_clos ]; apply Tlt_Tle_compat with (M.Term f x); try assumption; apply Tle_mono; apply stable_monotone_R_list with R_rules; assumption. Qed.
imports: Coq(Setoid List Relations Wellfounded PeanoNat) CoLoR(weaved_relation list_permut terminaison)