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