proposition: Lemma Vbuild_tail n (gen : forall i, i < S n -> A) : Vtail (Vbuild gen) = Vbuild (fun i ip => gen (S i) (NatCompat.lt_n_S ip)).
proof: Proof. apply Veq_nth; intros. rewrite Vnth_tail, !Vbuild_nth. refl. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)