proposition: Lemma vint_cast_typ : forall n (Ts : Tys n) n' (h : n=n') p (ts : Tes p), vint (Vcast Ts h) ts <-> vint Ts ts.
proof: Proof. induction Ts; intros n' e p ts. subst. rewrite Vcast_refl. refl. destruct n'. discr. rewrite Vcast_cons. simpl. destruct ts. refl. rewrite IHTs. refl. Qed.
imports: Coq(Morphisms Basics Lia) CoLoR(SN VecUtil LogicUtil SetUtil)