proposition: Lemma vint_sub_typ_intro : forall n (Ts : Tys n) p (ts : Tes p) (h : 0+p<=n), vint Ts ts -> vint (Vsub Ts h) ts.
proof: Proof. intros n Ts p ts h i. apply vint_intro_nth. refl. intros j j1 j2. rewrite Vnth_sub. apply vint_elim_nth. hyp. Qed.
imports: Coq(Morphisms Basics Lia) CoLoR(SN VecUtil LogicUtil SetUtil)