proposition: Lemma vint_sub_term_intro : forall n (Ts : Tys n) p (ts : Tes p) q (h : 0+q<=p), vint Ts ts -> vint Ts (Vsub ts h).
proof: Proof. intros n Ts p ts q h hts. apply vint_intro_nth. gen (vint_le hts). lia. intros j jn jq. rewrite Vnth_sub. apply vint_elim_nth. hyp. Qed.
imports: Coq(Morphisms Basics Lia) CoLoR(SN VecUtil LogicUtil SetUtil)