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