fact: Definition Trel_stable (R1 R2 : relation M.term) := forall (t1 t2 : M.term) (sigma : M.substitution), R1 t1 t2 -> R2 (M.apply_subst sigma t1) (M.apply_subst sigma t2).
imports: Coq(Setoid List Relations Wellfounded PeanoNat) CoLoR(weaved_relation list_permut terminaison)