proposition: Lemma output_arrow_elim : forall n (A B C : Ty), output A n = B ~~> C -> output A (S n) = C /\ exists h : S n <= arity A, Vnth (inputs A) h = B.
proof: Proof. induction n; destruct A; intros B C; rewrite ?output_Base; try discr; simpl; intro e. inversion e; subst. split. refl. ex (le_n_S (le_0_n (arity C))). refl. destruct (IHn _ _ _ e) as [h1 [h2 h3]]. split. revert h1. destruct A2; auto. ex (le_n_S h2). rewrite <- h3. apply Vnth_eq. refl. Qed.
imports: Coq(Relations) CoLoR(VecUtil LogicUtil OrdUtil NatUtil)