proposition: Lemma vint_app_intro : forall n (Ts : Tys n) p (ts : Tes p) q (us : Tes q) (h : p+q <= n), vint Ts ts -> vint (Vsub Ts h) us -> vint Ts (Vapp ts us).
proof: Proof. induction Ts; simpl. destruct ts; simpl; intros q us i. assert (q=0). lia. subst. VOtac. fo. lia. destruct ts; simpl; intros q us i. destruct us; simpl. fo. rewrite Vsub_cons. intuition. eapply vint_sub_typ_elim. apply H2. rewrite Vsub_cons. intuition. eapply IHTs. hyp. apply H0. Qed.
imports: Coq(Morphisms Basics Lia) CoLoR(SN VecUtil LogicUtil SetUtil)