proposition: Lemma int_arrow : forall V v n, n <= arity V -> (forall vs : Tes n, vint (inputs V) vs -> int (output V n) (apps v vs)) -> int V v.
proof: Proof. induction V; simpl; intros v n hn hv. assert (n=0). lia. subst n. change (I s (apps v Vnil)). apply hv. auto. destruct n. gen (hv Vnil). fo. intros v1 h1. apply IHV2 with (n:=n). lia. intros vs hvs. change (int (output V2 n) (apps v (Vcons v1 vs))). apply hv. fo. Qed.
imports: Coq(Morphisms Basics Lia) CoLoR(SN VecUtil LogicUtil SetUtil)