proposition: Lemma vint_intro_nth : forall n (Ts : Tys n) p (ts : Tes p), p <= n -> (forall j (jn : j<n) (jp : j<p), int (Vnth Ts jn) (Vnth ts jp)) -> vint Ts ts.
proof: Proof. induction Ts; destruct ts; intros a b; simpl; auto. lia. split. assert (p: 0<S n). lia. assert (q:0<S n0). lia. gen (b _ p q). auto. apply IHTs. lia. intros j p q. assert (p': S j<S n). lia. assert (q':S j<S n0). lia. gen (b _ p' q'). rewrite 2!Vnth_cons. destruct (NatUtil.lt_ge_dec 0 (S j)). 2: lia. assert (c : Vnth Ts (Vnth_cons_tail_aux p' l) = Vnth Ts p). apply Vnth_eq. lia. assert (d : Vnth ts (Vnth_cons_tail_aux q' l) = Vnth ts q). apply Vnth_eq. lia. rewrite c, d. auto. Qed.
imports: Coq(Morphisms Basics Lia) CoLoR(SN VecUtil LogicUtil SetUtil)