proposition: Lemma R_stable_list : forall l1 l2, one_step_list (EqtT.one_step R_rules) l1 l2 -> one_step_list Tle (map inject_term l1) (map inject_term l2).
proof: Proof. intros l1 l2 H; induction H; [ left | right; assumption ]; apply opT.stable_monotone_R_term with (O:=Tle_inject) in H; try assumption; apply Tle_inject_mono. Qed.
imports: Coq(Setoid List Relations Wellfounded PeanoNat) CoLoR(weaved_relation list_permut terminaison)