proposition: Lemma vterm_fill : forall t c, vterm_of_aterm (afill c t) = fill (vcont_of_acont c) (vterm_of_aterm t).
proof: Proof. induction c. refl. simpl afill. rewrite vterm_fun, vterms_cast, vterms_app. simpl. apply args_eq. apply appr_eq. rewrite IHc. refl. Qed.
imports: CoLoR(LogicUtil ListUtil VecUtil SN)