fact: Definition projection (t : term) : term := match t with | Var _ => t | Term f l => match nth_error l (P f) with | Some tf => tf | None => t end end.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term_spec equational_theory_spec dp) CoLoR(NatCompat)