proposition: Lemma arrow_output : forall T p q (h : p+q<=arity T), arrow (Vsub (inputs T) h) (output T (p+q)) = output T p.
proof: Proof. induction T; simpl; intros p q h. assert (p=0). lia. assert (q=0). lia. subst. refl. destruct p; simpl. destruct q; simpl. refl. rewrite Vsub_cons, IHT2. refl. rewrite Vsub_cons, IHT2. refl. Qed.
imports: Coq(Relations) CoLoR(VecUtil LogicUtil OrdUtil NatUtil)