proposition: Lemma Vin_first_position_aux : forall n (ys : vector A n) k, Vin x ys -> exists i, Vfirst_position_aux (eq_dec x) k ys = Some i.
proof: Proof. induction ys as [|y ys]; intro k; simpl. fo. intros [h|h]; destruct (eq_dec x y). subst y. exists k. refl. cong. exists k. refl. fo. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)