proposition: Lemma rpo_eq_stable_afs : Sdp.opT.Trel_stable R_rules Tle_inject.
proof: Proof. intros t1 t2 sigma H; unfold Tle_inject; unfold inject_term; rewrite Sdp.inject_subst; rewrite Sdp.inject_subst; unfold rpo_eq_afs; unfold afs; rewrite AfsM.afs_subst; rewrite AfsM.afs_subst; apply Rpo.rpo_eq_subst; apply rules_decrease; assumption. Qed.
imports: Coq(Setoid List Relations Lia Arith) CoLoR(weaved_relation list_permut terminaison)