proposition: Lemma vterm_fun : forall f ts, vterm_of_aterm (AFun f ts) = VFun f (vterms_of_aterms ts).
proof: Proof. intros. simpl. apply args_eq. generalize dependent (arity f). induction ts; simpl; auto. Qed.
imports: CoLoR(LogicUtil ListUtil VecUtil SN)