proposition: Lemma vint_pos : forall n (Ts : Tys n) p (ts : Tes p), Vforall (pos a) Ts -> vint I Ts ts -> vint J Ts ts.
proof: Proof. intros n Ts p ts h. destruct (vint_mon Ts ts) as [i _]. fo. Qed.
imports: Coq(Morphisms Basics Lia) CoLoR(SN VecUtil LogicUtil SetUtil)