proposition: Lemma rpo_stable_afs : Ext.op.Trel_stable dps rpo_afs.
proof: Proof. intros t1 t2 sigma H; unfold rpo_afs; unfold afs; rewrite Afs.afs_subst; rewrite Afs.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)