proposition: Lemma terms_of_aterms_cast : forall n (ts : aterms n) p (e : n=p), terms_of_aterms (Vcast ts e) = terms_of_aterms ts.
proof: Proof. induction ts; destruct p; simpl; intros; try discr. rewrite Vcast_refl. refl. inversion e. subst p. rewrite Vcast_cons. simpl. rewrite IHts. refl. Qed.
imports: CoLoR(LogicUtil ATerm VecUtil) CoLoR(term_spec EqUtil) CoLoR(NatUtil) Coq(List Relations) CoLoR(term SN ASubstitution)