proposition: Lemma vint_typs_eq_cast : forall n (Ts : Tys n) m (Us : Tys m) (h : n=m) p (ts : Tes p), vint Us ts -> Us = Vcast Ts h -> vint Ts ts.
proof: Proof. intros n Ts m Us h p ts i. subst. rewrite Vcast_refl. intro; subst. hyp. Qed.
imports: Coq(Morphisms Basics Lia) CoLoR(SN VecUtil LogicUtil SetUtil)