proposition: Lemma vterms_map : forall (A : Set) (f : A -> aterm) n (v : vector A n), vterms_of_aterms (Vmap f v) = List.map (fun x => vterm_of_aterm (f x)) (list_of_vec v).
proof: Proof. induction v; simpl. refl. apply tail_eq. apply IHv. Qed.
imports: CoLoR(LogicUtil ListUtil VecUtil SN)