proposition: Lemma Vbuild_nth : forall n gen i (ip : i < n), Vnth (Vbuild gen) ip = gen i ip.
proof: Proof. induction n; intros gen i ip. lia. destruct i; simpl. f_equal. apply lt_unique. rewrite IHn. f_equal. apply lt_unique. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)