fact: Definition mark_term (t : term) : term := match t with | Var x => Var x | Term f l => Term (mark f) l end.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec) CoLoR(NatCompat)