proposition: Lemma vint_sub_typ_elim : forall n (Ts : Tys n) p (ts : Tes p) (h : 0+p<=n), vint (Vsub Ts h) ts -> vint Ts ts.
proof: Proof. intros n Ts p ts h. rewrite 2!vint_eq; try lia. intuition. gen (H _ jp jp). rewrite Vnth_sub. erewrite Vnth_eq. intro i; apply i. refl. Qed.
imports: Coq(Morphisms Basics Lia) CoLoR(SN VecUtil LogicUtil SetUtil)