fact: Definition Trel_monotone (R : relation M.term) := forall (f : M.symbol) (l1 l2 : list M.term), one_step_list R l1 l2 -> R (M.Term f l1) (M.Term f l2).
imports: Coq(Setoid List Relations Wellfounded PeanoNat) CoLoR(weaved_relation list_permut terminaison)