proposition: Lemma vint_eq : forall n (Ts : Tys n) p (ts : Tes p), p <= n -> (vint Ts ts <-> (forall j (jn : j<n) (jp : j<p), int (Vnth Ts jn) (Vnth ts jp))).
proof: Proof. intros n Ts p ts pn. split. apply vint_elim_nth. apply vint_intro_nth. hyp. Qed.
imports: Coq(Morphisms Basics Lia) CoLoR(SN VecUtil LogicUtil SetUtil)