proposition: Lemma vred_of_ared : forall t u, ared R t u -> vred S (vterm_of_aterm t) (vterm_of_aterm u).
proof: Proof. intros. ATrs.redtac. subst t. subst u. rewrite !vterm_fill, !vterm_subs. apply red_rule. change (List.In (vrule_of_arule (ATrs.mkRule l r)) S). unfold S. apply in_map. hyp. Qed.
imports: CoLoR(LogicUtil ListUtil VecUtil SN)