fact: Fixpoint Vbuild n : (forall i, i<n -> A) -> vector A n := match n as n return (forall i, i<n -> A) -> vector A n with | 0 => fun _ => Vnil | S p => fun gen => Vcons (gen 0 (Nat.lt_0_succ p)) (Vbuild (fun i ip => gen (S i) (NatCompat.lt_n_S ip))) end.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)