proposition: Lemma Vin_first_position : forall n (ys : vector A n), Vin x ys -> exists i, Vfirst_position (eq_dec x) ys = Some i.
proof: Proof. intros n ys. apply Vin_first_position_aux. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)