proposition: Lemma vint_le : forall n (Ts : Tys n) p (ts : Tes p), vint Ts ts -> p <= n.
proof: Proof. induction Ts; destruct ts; simpl; try lia. intros [h1 h2]. gen (IHTs _ _ h2). lia. Qed.
imports: Coq(Morphisms Basics Lia) CoLoR(SN VecUtil LogicUtil SetUtil)