proposition: Lemma vterms_app : forall n1 (ts1 : aterms n1) n2 (ts2 : aterms n2), vterms_of_aterms (Vapp ts1 ts2) = vterms_of_aterms ts1 ++ vterms_of_aterms ts2.
proof: Proof. induction ts1; simpl. refl. intros. apply tail_eq. apply IHts1. Qed.
imports: CoLoR(LogicUtil ListUtil VecUtil SN)