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