proposition: Lemma wf_union : well_founded (Eqt.one_step R_union).
proof: Proof. apply Lex.wf_union_R with (Tle:=rpo_eq_afs) (Tlt:=rpo_afs) (R_rules:=R_rules) (R_large:=R_large); try assumption. unfold rpo_afs; apply Inverse_Image.wf_inverse_image; apply Rpo.wf_rpo; apply (prec_wf prec). apply Afs.Tle_monotone_afs; [ apply Ext.rpo_eq_monotone | apply Ext.rpo_eq_trans ]. apply Afs.Tlt_monotone_afs; [ apply Ext.rpo_monotone | intros x y z; apply Rpo.rpo_trans ]. apply Afs.Tlt_Tle_compat_afs; apply Ext.rpo_rpo_eq_compat. apply rpo_stable_afs. 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_large_decrease; assumption. Qed.
imports: Coq(Setoid List Relations Lia Arith) CoLoR(weaved_relation list_permut terminaison)