proposition: Lemma Vbuild_head : forall n (gen : forall i, i < S n -> A), Vhead (Vbuild gen) = gen 0 (Nat.lt_0_succ n).
proof: Proof. intros n gen. rewrite Vhead_nth, Vbuild_nth. refl. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)