proposition: Lemma vint_mon : forall n (Ts : Tys n) p (ts : Tes p), (Vforall (pos a) Ts -> vint I Ts ts -> vint J Ts ts) /\ (Vforall (neg a) Ts -> vint J Ts ts -> vint I Ts ts).
proof: Proof. induction Ts; intro p; destruct ts; simpl. fo. fo. fo. destruct (IHTs _ ts) as [a1 a2]. split; intros [h1 h2] [i1 i2]. split. apply int_pos; hyp. apply a1; hyp. split. apply int_neg; hyp. apply a2; hyp. Qed.
imports: Coq(Morphisms Basics Lia) CoLoR(SN VecUtil LogicUtil SetUtil)