proposition: Lemma vterm_subs : forall s t, vterm_of_aterm (asub s t) = vsub (vsubs_of_asubs s) (vterm_of_aterm t).
proof: Proof. intros. pattern t. apply ATerm.term_ind with (Q := fun n (ts : aterms n) => vterms_of_aterms (Vmap (asub s) ts) = List.map (vsub (vsubs_of_asubs s)) (vterms_of_aterms ts)). refl. intros. simpl ASubstitution.sub. rewrite !vterm_fun. simpl. apply args_eq. exact H. refl. intros. simpl. rewrite H. apply tail_eq. exact H0. Qed.
imports: CoLoR(LogicUtil ListUtil VecUtil SN)