proposition: Lemma Vbuild_in n gen x : Vin x (Vbuild gen) -> exists i, exists ip : i < n, x = gen i ip.
proof: Proof. intro hx. apply Vin_nth in hx. destruct hx as [i [i_n hi]]. ex i i_n. rewrite <- Vbuild_nth. auto. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)