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