fact: Fixpoint term_of_aterm (t : aterm) := match t with | AVar x => Var x | Fun f ts => let fix terms_of_aterms n (ts : aterms n) := match ts with | Vnil => nil | Vcons u us => term_of_aterm u :: terms_of_aterms _ us end in Term f (terms_of_aterms (arity f) ts) end.
imports: CoLoR(LogicUtil ATerm VecUtil) CoLoR(term_spec EqUtil) CoLoR(NatUtil) Coq(List Relations) CoLoR(term SN ASubstitution)