fact: Fixpoint sub_of_asub (s : ASubstitution.substitution Sig) n := match n with | 0 => nil | S n' => (n', term_of_aterm (s n')) :: sub_of_asub s n' end.
imports: CoLoR(LogicUtil ATerm VecUtil) CoLoR(term_spec EqUtil) CoLoR(NatUtil) Coq(List Relations) CoLoR(term SN ASubstitution)