fact: Definition sigma_inject (sigma : T.substitution) : M.substitution := map (fun p => (fst p, inject_term (snd p))) sigma.
imports: Coq(Setoid List Relations Wellfounded PeanoNat) CoLoR(weaved_relation list_permut terminaison)