proposition: Lemma rtc_R_step : forall t f l1 l2, Tlt_mark t (T.Term f l1) -> refl_trans_clos (one_step_list (EqtT.one_step R_rules)) l1 l2 -> Tlt_mark t (T.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 (mark_term (inject_term (T.Term f x))); try assumption; simpl; apply Tle_mono; apply R_stable_list; assumption. Qed.
imports: Coq(Setoid List Relations Wellfounded PeanoNat) CoLoR(weaved_relation list_permut terminaison)