proposition: Lemma vterms_cast : forall n (ts : aterms n) m (h : n=m), vterms_of_aterms (Vcast ts h) = vterms_of_aterms ts.
proof: Proof. induction ts; intros; destruct m; try discr. rewrite Vcast_refl. refl. rewrite Vcast_cons. simpl. apply tail_eq. apply IHts. Qed.
imports: CoLoR(LogicUtil ListUtil VecUtil SN)