fact: Definition mark_term (t : M.term) : M.term := match t with | M.Term f ts => M.Term (mark_symb f) ts | _ => t end.
imports: Coq(Setoid List Relations Wellfounded PeanoNat) CoLoR(weaved_relation list_permut terminaison)