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