proposition: Lemma vint_elim_nth : forall n (Ts : Tys n) p (ts : Tes p), vint Ts ts -> forall j (jn : j<n) (jp : j<p), int (Vnth Ts jn) (Vnth ts jp).
proof: Proof. induction Ts; destruct ts; simpl Def.vint; intros hts j jn jp; intuition. destruct j; simpl. hyp. apply IHTs. hyp. Qed.
imports: Coq(Morphisms Basics Lia) CoLoR(SN VecUtil LogicUtil SetUtil)