proposition: Lemma Vin_build : forall n (gen : forall i, i < n -> A) x, (exists i (ip : i < n), x = gen i ip) -> Vin x (Vbuild gen).
proof: Proof. intros n gen x [i [i_n hi]]. subst x. rewrite <- Vbuild_nth. apply Vnth_in. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)