proposition: Lemma vint_sub_intro : forall n (Ts : Tys n) p (ts : Tes p), vint Ts ts -> forall i k (h : i+k<=n) k' (h' : i+k'<= p), k'<=k -> vint (Vsub Ts h) (Vsub ts h').
proof: Proof. intros n Ts p ts a i k h k' h' b. apply vint_intro_nth. hyp. intros j jk jk'. rewrite 2!Vnth_sub. apply vint_elim_nth. hyp. Qed.
imports: Coq(Morphisms Basics Lia) CoLoR(SN VecUtil LogicUtil SetUtil)