proposition: Lemma rpo_stable_afs : Sdp.opT.Trel_stable dps Tlt_mark.
proof: Proof. intros t1 t2 sigma H; unfold Tlt_mark; unfold inject_term; unfold mark_term; rewrite Sdp.mark_inject_subst; [| apply (dps_non_variable H) ]; rewrite Sdp.mark_inject_subst; [| apply (dps_non_variable H) ]; unfold rpo_afs; unfold afs; rewrite AfsM.afs_subst; rewrite AfsM.afs_subst; apply Rpo.rpo_subst; apply dps_strictly_decrease; assumption. Qed.
imports: Coq(Setoid List Relations Lia Arith) CoLoR(weaved_relation list_permut terminaison)