fact: Fixpoint inject_term (t : T.term) : M.term := match t with | T.Term f ts => M.Term (inject_symb f) (List.map inject_term ts) | T.Var i => M.Var i end.
imports: Coq(Setoid List Relations Wellfounded PeanoNat) CoLoR(weaved_relation list_permut terminaison)