proposition: Lemma terms_of_aterms_app : forall n (ts : aterms n) p (us : aterms p), terms_of_aterms (Vapp ts us) = terms_of_aterms ts ++ terms_of_aterms us.
proof: Proof. induction ts; simpl; intros. refl. rewrite IHts. refl. Qed.
imports: CoLoR(LogicUtil ATerm VecUtil) CoLoR(term_spec EqUtil) CoLoR(NatUtil) Coq(List Relations) CoLoR(term SN ASubstitution)