proposition: Lemma int_apps : forall n (vs : Tes n) v (Vs : Tys n) A, vint Vs vs -> int (arrow Vs A) v -> int A (apps v vs).
proof: Proof. induction vs; simpl; intros v Vs V. VOtac. simpl. auto. VSntac Vs. simpl. intros [h1 h2] h3. eapply IHvs. apply h2. apply h3. hyp. Qed.
imports: Coq(Morphisms Basics Lia) CoLoR(SN VecUtil LogicUtil SetUtil)