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