proposition: Lemma wf : well_founded (Eqt.one_step R_rules).
proof: Proof. apply Lex.wf_R with (Tlt:=rpo_afs). apply Inverse_Image.wf_inverse_image with (f:=afs); apply Rpo.wf_rpo; apply (prec_wf prec ). apply Afs.Tlt_monotone_afs; [ apply Ext.rpo_monotone | intros x y z; apply Rpo.rpo_trans ]. apply rpo_stable_afs. Qed.
imports: Coq(Setoid List Relations Lia Arith) CoLoR(weaved_relation list_permut terminaison)