proposition: Lemma Vin_nth : forall n (v : vector A n) a, Vin a v -> exists i, exists ip : i < n, Vnth v ip = a.
proof: Proof. induction n; intros. VOtac. destruct H. VSntac v. rewrite H0 in H. destruct H. exists 0. exists (Nat.lt_0_succ n). simpl. congruence. destruct (IHn (Vtail v) a H) as [j [jp v_j]]. exists (S j). exists (NatCompat.lt_n_S jp). simpl. rewrite lt_Sn_nS. hyp. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)